1989 · 162 citations · 16 references
ComputingComputer EngineeringComputer ScienceFormal MethodsLogicReal-time SystemsDeductive VerificationModal LogicModel CheckingPredicate LogicReal-time Systems DesignTemporal LogicOperatorsReactive SystemsReal-time Systems VerificationReal-time Temporal LogicTemporal Logic SpecificationTemporal Logic VerificationTemporal OperatorsTemporal Verification
TPTL is both a natural language for specification and a suitable formalism for verification. We introduce a temporal logic for the specification of real‑time systems. Our logic, TPTL, uses a freeze quantifier that binds a variable to the local time, and we provide a tableau‑based decision procedure and a model‑checking algorithm. Several generalizations of TPTL are shown to be highly undecidable.
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.
16
Introduction to automata theory, languages, and computation
Computer Languages · 1980 · 6.9K citations
The temporal logic of programs
Amir Pnueli · 1977 · 5.7K citations
The complexity of propositional linear temporal logics
A. Prasad Sistla, E. M. Clarke · Journal of the ACM · 1985 · 1.1K citations · Full text