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 explicit existential
and universal quantification over selected paths, namely, those that
are possible outcomes of games 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, preceding the temporal operator ``eventually'' by an
alternating-time path quantifier we can specify that a system can
reach a state satisfying a predicate $\varphi$ *no matter how the
environment behaves*. In other words, in the game between the system
and the environment, the system has a strategy to reach a
$\varphi$-state.
Similarly, the problems of receptiveness, controllability, and
realizability all can be formulated,
naturally and uniformly, as model-checking problems for
alternating-time logics.

Depending on whether we admit arbitrary nesting of alternating-time path quantifiers and temporal operators, we obtain the two alternating-time temporal logics ATL and ATL*. We interpret formulas of ATL and \atlsr with respect to two models of open systems: synchronous and asynchronous. For synchronous systems, the expressive power of ATL beyond CTL comes at no cost: we give a symbolic fixpoint-computation procedure for ATL model checking, and prove that the ATL model-checking problem is linear in the size of both the structure and the formula. For asynchronous systems, the symbolic procedure involves nested fixed-point calculation and the complexity is quadratic. This makes ATL an obvious candidate for the verification of open systems, just like CTL is widely used for the verification of closed systems. It also suggests, for the first time, an interesting class of properties of open systems that can be checked efficiently. In the case of ATL*, the model-checking problem is closely related to the synthesis problem for linear-time temporal logic, and it comes, for both synchronous and asynchronous systems, at the cost of an extra exponential beyond CTL* model checking, at 2EXPTIME.

A preliminary version appears in the
*Proceedings of the
38th Annual IEEE Symposium on Foundations of Computer Science*
(FOCS'97), pp. 100-109, 1997.

An extended version appears in
*Compositionality -- The
Significant Difference,* LNCS 1536, pp. 23--60,
Springer-Verlag, 1999.