A really temporal logic
Alur R, Henzinger TA. 1994. A really temporal logic. Journal of the ACM. 41(1), 181–204.
Download
No fulltext has been uploaded. References only!
Journal Article
| Published
| English
Scopus indexed
Author
Alur, Rajeev;
Henzinger, Thomas AISTA 
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.
Publishing Year
Date Published
1994-01-01
Journal Title
Journal of the ACM
Acknowledgement
We thank Zohar Manna, Amir Pnueli, and David Dill for their guidance. Moshe Vardi and Joe Halpern gave us very helpful advice for refining our undecidability results; in particular, they pointed out to us the completeness of a problem on Turing machines.
Volume
41
Issue
1
Page
181 - 204
ISSN
IST-REx-ID
Cite this
Alur R, Henzinger TA. A really temporal logic. Journal of the ACM. 1994;41(1):181-204. doi:10.1145/174644.174651
Alur, R., & Henzinger, T. A. (1994). A really temporal logic. Journal of the ACM. ACM. https://doi.org/10.1145/174644.174651
Alur, Rajeev, and Thomas A Henzinger. “A Really Temporal Logic.” Journal of the ACM. ACM, 1994. https://doi.org/10.1145/174644.174651.
R. Alur and T. A. Henzinger, “A really temporal logic,” Journal of the ACM, vol. 41, no. 1. ACM, pp. 181–204, 1994.
Alur R, Henzinger TA. 1994. A really temporal logic. Journal of the ACM. 41(1), 181–204.
Alur, Rajeev, and Thomas A. Henzinger. “A Really Temporal Logic.” Journal of the ACM, vol. 41, no. 1, ACM, 1994, pp. 181–204, doi:10.1145/174644.174651.
Google Scholar