## Symbolic Model Checking for Real-Time Systems

*
Thomas A. Henzinger,
Xavier Nicollin, Joseph Sifakis, and Sergio Yovine*

We describe finite-state programs over real-numbered time in a
guarded-command language with real-valued clocks or, equivalently, as
finite automata with real-valued clocks. Model checking answers the
question which states of a real-time program satisfy a branching-time
specification (given in an extension of CTL with clock variables). We
develop an algorithm that computes this set of states symbolically as
a fixpoint of a functional on state predicates, without constructing
the state space.

For this purpose, we introduce a mu-calculus on computation trees over
real-numbered time. Unfortunately, many standard program properties,
such as response for all nonzeno execution sequences (during which
time diverges), cannot be characterized by fixpoints: we show that the
expressiveness of the timed mu-calculus is incomparable to the
expressiveness of timed CTL. Fortunately, this result does not impair
the symbolic verification of "implementable" real-time programs--those
whose safety constraints are machine-closed with respect to diverging
time and whose fairness constraints are restricted to finite upper
bounds on clock values. All timed CTL properties of such programs are
shown to be computable as finitely approximable fixpoints in a simple
decidable theory.

*Information and Computation* 111:193-244, 1994.
A preliminary version appeared in the
*Proceedings of the
Seventh Annual Symposium on Logic in Computer Science*
(LICS), IEEE Computer Society Press, 1992, pp. 394-406.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 1992 IEEE,
1994 Academic Press.