Alternating-Time Temporal Logic
-------------------------------
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. Also the problems of receptiveness, realizability, and
controllability can be formulated as model-checking problems for
alternating-time formulas.
Depending on whether we admit arbitrary nesting of selective path
quantifiers and temporal operators, we obtain the two alternating-time
temporal logics ATL and ATL*. We interpret the formulas of ATL and
ATL* with respect to two models of composition for open systems,
synchronous and asynchronous. For synchronous systems, the expressive
power of ATL beyond CTL comes at no cost: the model-checking
complexity of synchronous ATL is linear in the size of the system and
the length of the formula. The symbolic model-checking algorithm for
CTL extends with few modifications to synchronous ATL, and with some
work, also to asynchronous ATL, whose model-checking complexity is
quadratic. This makes ATL an obvious candidate for the automatic
verification of open systems. 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 for both synchronous
and asynchronous systems.