A really temporal logic
- 1 January 1989
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 164-169
- https://doi.org/10.1109/sfcs.1989.63473
Abstract
A real-time temporal logic for the specification of reactive systems is introduced. The novel feature of the logic, TPTL, is the adoption of temporal operators as quantifiers over time variables; every modality binds a variable to the time(s) it refers to. TPTL is demonstrated to be both a natural specification language and a suitable formalism for verification and synthesis. A tableau-based decision procedure and model-checking algorithm for TPTL are presented. Several generalizations of TPTL are shown to be highly undecidable.Keywords
This publication has 5 references indexed in Scilit:
- A really temporal logicPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1989
- Propositional dynamic logic of nonregular programsJournal of Computer and System Sciences, 1983
- Real-time programming and asynchronous message passingPublished by Association for Computing Machinery (ACM) ,1983
- Temporal logic can be more expressiveInformation and Control, 1983
- The temporal logic of programsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1977