Modal Logics and Topological Semantics for Hybrid Systems
Abstract
This paper introduces the logic of a control action S4F and the logic of a continuous control action S4C on the state space of a dynamical system. The state space is represented by a topological space (X, T) and the control action by a function f from X to X. We present an intended topological semantics and a Kripke semantics, give both a Hilbert style axiomatization and Gentzen style sequent calculus for S4F and S4C, and prove completeness with respect to both semantics a cut elimination for the sequent calculi, and decidability of the logics.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 01, 1997
- Accession Number
- ADA344355
Entities
People
- A. Nerode
- Jennifer M. Davoren
- Sergei N. Artemov
Organizations
- University of California, Berkeley