Modal Logics and Topological Semantics for Hybrid Systems
Sergei Nikolaevich Artemov, Jennifer M. Davoren, Anil Nerode · 1997
In this paper, we introduce 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 here 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 and Gentzen-style axiomatization for S4F and S4C, prove completeness with respect to both semantics as well as a cut-elimination for the corresponding sequent calculi and show the logics to be decidable. 1 Introduction Let L2 be the propositional modal language generated from a countable set PV of propositional variables, the propositional constant ? (falsum), the propositional connective ! (implication), and the modal operator 2. Let L2a be the propositional language extending L2 which includes, in addition, a new modal operator [a]. Let S4 denote the subset of L2a consisting of all formulas derivable from a standard axi...