A really temporal logic

R. Alur, T.A. Henzinger, Journal of the ACM 41 (1994) 181–204.

Download
No fulltext has been uploaded. References only!

Journal Article | Published
Author
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
Volume
41
Issue
1
Page
181 - 204
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, 41(1), 181–204. https://doi.org/10.1145/174644.174651
Alur, Rajeev, and Thomas A Henzinger. “A Really Temporal Logic.” Journal of the ACM 41, no. 1 (1994): 181–204. 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, 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.

Link(s) to Main File(s)
Access Level
Restricted Closed Access

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar