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.