## Half-Order Modal Logic: How To Prove Real-Time Properties

*
Thomas A. Henzinger*

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
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 *half-order* modal logic.

As a special case, we obtain the real-time temporal logic TPTL: 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.

*Ninth Annual Symposium on Principles of Distributed Computing*
(PODC), ACM Press, 1990, pp. 281-296.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 1990 ACM