A really temporal logic Journal Article


Author(s): Alur, Rajeev; Henzinger, Thomas A
Article Title: A really temporal logic
Affiliation
Abstract: We introduce a temporal logic for the specification of real-time systems. Our logic, TPTL, employs a novel quantifier construct for referencing time: the freeze quantifier binds a variable to the time of the local temporal context. TPTL is both a natural language for specification and a suitable formalism for verification. We present a tableau-based decision procedure and a model-checking algorithm for TPTL. Several generalizations of TPTL are shown to be highly undecidable.
Journal Title: Journal of the ACM
Volume: 41
Issue 1
ISSN: 0004-5411
Publisher: ACM  
Date Published: 1994-01-01
Start Page: 181
End Page: 204
URL:
DOI: 10.1145/174644.174651
Open access: no
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
Related IST Austria Work