A really temporal logic
- 2 January 1994
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 41 (1) , 181-203
- https://doi.org/10.1145/174644.174651
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.Keywords
This publication has 8 references indexed in Scilit:
- What good are digital clocks?Published by Springer Nature ,1992
- Logics and models of real time: A surveyPublished by Springer Nature ,1992
- Presburger arithmetic with unary predicates is Π11 completeThe Journal of Symbolic Logic, 1991
- Specifying real-time properties with metric temporal logicReal-Time Systems, 1990
- Safety analysis of timing properties in real-time systemsIEEE Transactions on Software Engineering, 1986
- The complexity of propositional linear temporal logicsJournal of the ACM, 1985
- Synthesis of Communicating Processes from Temporal Logic SpecificationsACM Transactions on Programming Languages and Systems, 1984
- Proving Liveness Properties of Concurrent ProgramsACM Transactions on Programming Languages and Systems, 1982