Alternating-time Temporal Logic

Temporal logic comes in two varieties: linear-time temporal logic assumes implicit universal quantification over all paths that are generated by system moves; branching-time temporal logic allows explicit existential and universal quantification over all paths. We introduce a third, more general variety of temporal logic: alternating-time temporal logic offers selective quantification over those paths that are possible outcomes of games, such as the game in which the system and the environment alternate moves. While linear-time and branching-time logics are natural specification languages for closed systems, alternating-time logics are natural specification languages for open systems. For example, by preceding the temporal operator "eventually" with a selective path quantifier, we can specify that in the game between the system and the environment, the system has a strategy to reach a certain state. Also the problems of receptiveness, realizability, and controllability can be formulated as model-checking problems for alternating-time formulas.

Authors

• Rajeev Alur
• Thomas A. Henzinger
• Orna Kupferman

Keywords

• Logic
• Open systems
• Power system modeling
• Specification languages
• Controllability
• Costs
• Engineering profession
• Contracts
• Information science
• Debugging
• Temporal Logic
• Alternating-time Temporal Logic
• Operating System
• System Size
• Closed System
• Model Checking
• Synchronization Of Systems
• Formula Length
• Temporal Operators
• Universal Quantifier
• Asynchronous System
• Infinity
• System State
• Protagonist
• Fixed Point
• State Structures
• Set Of Calculations
• Set Of Agents
• Strategies Of Agents
• Infinite Sequence
• Type Of Formula
• Labeling Procedure