Logics and Models of Real Time: A Survey

We survey logic-based and automata-based languages and techniques for the speci cation and veri cation of real-time systems. In particular, we discuss three syntactic extensions of temporal logic: time-bounded operators, freeze quanti cation, and time variables. We also discuss the extension of nite-state machines with clocks and the extension of transition systems with time bounds on the transitions. All of the resulting notations can be interpreted over a variety of di erent models of time and computation, including linear and branching time, interleaving and true concurrency, discrete and continuous time. For each choice of syntax and semantics, we summarize the results that are known about expressive power, algorithmic nite-state veri cation, and deductive veri cation.

• Type: Conference
• Year: 1991
• Where: REX
• Authors: Rajeev Alur, Thomas A. Henzinger
• Keywords: Deductive Veri Cation, Distributed And Parallel Computing, Nite-state Veri Cation, REX 1991, Veri Cation