Half-Order Modal Logic: How to Prove Real-Time Properties

11 years 3 months ago
Half-Order Modal Logic: How to Prove Real-Time Properties
Abstract. We introduce a novel extension of propositional modal logic that is interpreted over Kripke structures in which a value is associated with every possible world. These values are, however, not treated as full rst-order objects they can be accessed only by a very restricted form of quanti cation: the \freeze" quanti er binds a variable to the value of the current world. We present a complete proof system for this (\half-order") modal logic. As a special case, we obtain the real-time temporal logic TPTL of AH89]: the models are restricted to in nite sequences of states, whose values are monotonically increasing natural numbers. The ordering relation between states is interpreted as temporal precedence, while the value associated with a state is interpreted as its \real" time. We extend our proof system to be complete for TPTL, and demonstrate how it can be used to derive real-time properties.
Thomas A. Henzinger
Added 11 Aug 2010
Updated 11 Aug 2010
Type Conference
Year 1990
Where PODC
Authors Thomas A. Henzinger
Comments (0)