Half-order modal logic: how to prove real-time properties
Tom Henzinger · 1990
We introduce a novel extension of propositional modal logic that is interpreted over Kripke structures in which a value is associated with every possible woxld.These values are, however, not treated as full first-order objects; they can be accessed only by a very restricted form of quantification:the "freeze" quantifier binds a variable to the value of the current world.We present a complete proof system for this ("hulf_o4er") modal logic.As a special case, we obtain the real-time temporal logic TPTL of [AH89]: the models are restricted to infinite 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.