## A Space-efficient On-the-Fly Algorithm for Real-Time Model Checking

*
Thomas A. Henzinger,
Orna Kupferman, and Moshe Y. Vardi*

In temporal-logic model checking, we verify the correctness of a
program with respect to a desired behavior by checking whether a
structure that models the program satisfies a temporal-logic formula
that specifies the behavior. The main practical limitation of model
checking is caused by the size of the state space of the program,
which grows exponentially with the number of concurrent components.
This problem, known as the state-explosion problem, becomes more
difficult when we consider real-time model checking, where the program
and the specification involve quantitative references to time. In
particular, when use timed automata to describe real-time programs and
we specify timed behaviors in the logic TCTL, a real-time extension of
the temporal logic CTL with clock variables, then the state space
under consideration grows exponentially not only with the number of
concurrent components, but also with the number of clocks and the
length of the clock constraints used in the program and the
specification. Two powerful methods for coping with the
state-explosion problem are *on-the-fly* and
*space-efficient* model checking. In on-the-fly model checking,
we explore only the portion of the state space of the program whose
exploration is essential for determining the satisfaction of the
specification. In space-efficient model checking, we store in memory
the minimal information required, preferring to spend time on
reconstructing information rather than spend space on storing it. In
this work we develop an automata-theoretic approach to TCTL model
checking that combines both methods. We suggest, for the first time,
a PSPACE on-the-fly model-checking algorithm for TCTL.

*Proceedings of the
Seventh International Conference on Concurrency Theory*
(CONCUR),
Lecture Notes in Computer Science 1119,
Springer, 1996, pp. 514-529.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 1996 Springer.