Skip to main content


eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item:
Title: Logics and Models of Real Time: A Survey
Authors: Alur, Rajeev
Henzinger, Thomas A.
Keywords: computer science
technical report
Issue Date: Jan-1992
Publisher: Cornell University
Abstract: We survey logic-based and automata-based languages and techniques for the specification and verification of real-time systems. In particular, we discuss three syntactic extensions of temporal logic: time-bounded operators, freeze quantification, and time variables. We also discuss the extension of finite-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 different 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 finite-state verification, and deductive verification.
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
92-1262.pdf3.55 MBAdobe PDFView/Open
92-1262.ps633.53 kBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.


© 2014 Cornell University Library Contact Us