Alternating-time temporal logic
Top Cited Papers
- 23 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 02725428,p. 100-109
- https://doi.org/10.1109/sfcs.1997.646098
Abstract
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.Keywords
This publication has 18 references indexed in Scilit:
- The model checker SPINIEEE Transactions on Software Engineering, 1997
- Composing specificationsACM Transactions on Programming Languages and Systems, 1993
- The control of discrete event systemsProceedings of the IEEE, 1989
- Automata-theoretic techniques for modal logics of programsJournal of Computer and System Sciences, 1986
- Automatic verification of finite-state concurrent systems using temporal logic specificationsACM Transactions on Programming Languages and Systems, 1986
- “Sometimes” and “not never” revisitedJournal of the ACM, 1986
- Checking that finite state concurrent programs satisfy their linear specificationPublished by Association for Computing Machinery (ACM) ,1985
- Results on the propositional μ-calculusTheoretical Computer Science, 1983
- Number of quantifiers is better than number of tape cellsJournal of Computer and System Sciences, 1981
- AlternationJournal of the ACM, 1981