Abstract: 
Temporal logic comes in two varieties: lineartime temporal logic assumes implicit universal quantification over all paths that are generated by the execution of a system; branchingtime temporal logic allows explicit existential and universal quantification over all paths. We introduce a third, more general variety of temporal logic: alternatingtime 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 lineartime and branchingtime logics are natural specification languages for closed systems, alternatingtime 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 modelchecking problems for alternatingtime formulas. Depending on whether or not we admit arbitrary nesting of selective path quantifiers and temporal operators, we obtain the two alternatingtime 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 modelchecking complexity of ATL is linear in the size of the game structure and length of the formula, and the symbolic modelchecking algorithm for CTL extends with few modifications to ATL. Over structures with weakfairness constraints, ATL model checking requires the solution of 1pair Rabin games, and can be done in polynomial time. Over structures with strongfairness constraints, ATL model checking requires the solution of games with Boolean combinations of Büchi conditions, and can be done in PSPACE. In the case of ATL*, the modelchecking problem is closely related to the synthesis problem for lineartime formulas, and requires doubly exponential time.
