*Rajeev Alur,
Thomas A. Henzinger,
and Orna Kupferman*

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. The problems of receptiveness, realizability, and
controllability can be formulated as model-checking problems for
alternating-time formulas. Depending on whether or not we admit
arbitrary nesting of selective path quantifiers and temporal
operators, we obtain the two alternating-time temporal logics ATL and
ATL*.

ATL and ATL* are interpreted over *concurrent game structures*. Every
state transition of a concurrent game structure results from a choice
of moves, one for each player. The players represent individual
components and the environment of an open system. Concurrent game
structures can capture various forms of synchronous composition for
open systems, and if augmented with fairness constraints, also
asynchronous composition. Over structures without fairness
constraints, the model-checking complexity of ATL is linear in the
size of the game structure and length of the formula, and the symbolic
model-checking algorithm for CTL extends with few modifications to
ATL. Over structures with weak-fairness constraints, ATL model
checking requires the solution of 1-pair Rabin games, and can be done
in polynomial time. Over structures with strong-fairness constraints,
ATL model checking requires the solution of games with Boolean
combinations of Buechi conditions, and can be done in PSPACE. In the
case of ATL*, the model-checking problem is closely related to the
synthesis problem for linear-time formulas, and requires doubly
exponential time.

*Journal of the ACM* 49:672-713, 2002.
Preliminary versions appeared in the
*Proceedings of the
38th Annual Symposium on Foundations of Computer Science*
(FOCS), IEEE Computer Society Press, 1997, pp. 100-109,
and in
*Compositionality: The Significant Difference*,
Lecture Notes in Computer Science 1536,
Springer, 1998, pp. 23-60.

Download inofficial, sometimes updated PostScript / PDF document. © 1997 IEEE, 1998 Springer, 2002 ACM.