A Really Temporal Logic

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. >

Authors

• Rajeev Alur
• Thomas A. Henzinger

Keywords

• Logic
• Real time systems
• Computer science
• Specification languages
• Contracts
• Temporal Logic
• Semantic
• Real-Time System
• Diamond
• Infinity
• Time Constraints
• Discrete-time
• Time Sequence
• Directed Graph
• Specific Language
• Decision Problem
• Global Variables
• Vertices
• Sequence Of States
• Starting State
• Successor States
• Model Checking
• Turing Machine
• Temporal Operators
• Asynchronous System