Alternating-time Temporal Logic

Rajeev Alur, Thomas A. Henzinger and Orna Kupferman

Journal of the ACM 49(5), 2002, pages 672-713

Used by the Cassting project

Temporal logics are a very powerful formalism for expressing properties to be checked in a computerized system. They usually come in two varieties: linear-time temporal logic assumes implicit universal quantification over all paths that are generated by the execution of a system; branching-time temporal logic allows explicit existential and universal quantification over all paths. This paper introduces 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 operators with a selective path quantifier, one can specify in ATL that in the game between the system and the environment, the system has a strategy to achieve a certain goal. The problems of receptiveness, realizability, and controllability can be formulated as model-checking problems for alternating-time formulas. Model-checking ATL is linear in the size of the game structure and in the length of the formula.