It's About Time: Real-Time Logics Reviewed

Thomas A. Henzinger

We summarize and reorganize some of the last decade's research on real-time extensions of temporal logic. Our main focus is on tableau constructions for model checking linear temporal formulas with timing constraints. In particular, we find that a great deal of real-time verification can be performed in polynomial space, but also that considerable care must be exercised in order to keep the real-time verification problem in polynomial space, or even decidable.

Proceedings of the Ninth International Conference on Concurrency Theory (CONCUR), Lecture Notes in Computer Science 1466, Springer, 1998, pp. 439-454.

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