Alur, Rajeev; Henzinger, Thomas AIST Austria ; Kupferman, Orna
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
100 - 109
FOCS: Foundations of Computer Science
Alur R, Henzinger TA, Kupferman O. Alternating-time temporal logic. In: IEEE; 1997:100-109. doi: 10.1109/SFCS.1997.646098
Alur, R., Henzinger, T. A., & Kupferman, O. (1997). Alternating-time temporal logic (pp. 100–109). Presented at the FOCS: Foundations of Computer Science, IEEE. https://doi.org/ 10.1109/SFCS.1997.646098
Alur, Rajeev, Thomas A Henzinger, and Orna Kupferman. “Alternating-Time Temporal Logic,” 100–109. IEEE, 1997. https://doi.org/ 10.1109/SFCS.1997.646098 .
R. Alur, T. A. Henzinger, and O. Kupferman, “Alternating-time temporal logic,” presented at the FOCS: Foundations of Computer Science, 1997, pp. 100–109.
Alur R, Henzinger TA, Kupferman O. 1997. Alternating-time temporal logic. FOCS: Foundations of Computer Science, 100–109.
Alur, Rajeev, et al. Alternating-Time Temporal Logic. IEEE, 1997, pp. 100–09, doi: 10.1109/SFCS.1997.646098 .