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 the execution of a system; 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&ast;.ATL and ATL&ast; 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 Bchi conditions, and can be done in PSPACE. In the case of ATL&ast;, the model-checking problem is closely related to the synthesis problem for linear-time formulas, and requires doubly exponential time.
Introduction
In 1977, Pnueli proposed to use linear-time temporal
logic (LTL) to specify requirements for reactive
systems [Pnu77]. A formula of LTL is interpreted
over a computation, which is an infinite sequence of
states. A reactive system satisfies an LTL formula if
all its computations do. Due to the implicit use of
universal quantification over the set of computations,
cannot express existential, or possibility, prop-
erties. Branching-time temporal logics, such as CTL
and CTL ? , do provide explicit quantification over the
set of computations [CE81, EH86]. For instance, for
a state predicate ', the CTL formula 83' requires
that a state satisfying ' is visited in all computa-
tions, and the CTL formula 93' requires that there
exists a computation that visits a state satisfying '.
The problem of model checking is to verify whether
a finite-state abstraction of a reactive system satisfies
a temporal-logic specification [CE81, QS81]. Efficient
model checkers exist for both LTL (e.g. SPIN [Hol97])
and CTL (e.g. SMV [McM93]), and are increasingly
being used as debugging aids for industrial designs.
The logics LTL and CTL have their natural interpretation
over the computations of closed systems,
where a closed system is a system whose behavior
is completely determined by the state of the system.
However, the compositional modeling and design of re-active
systems requires each component to be viewed
as an open system, where an open system is a system
that interacts with its environment and whose behavior
depends on the state of the system as well as the behavior
of the environment. Models for open systems,
such as CSP [Hoa85], I/O automata [Lyn96], and re-active
modules [AH96], distinguish between internal
nondeterminism, choices made by the system, and external
nondeterminism, choices made by the environ-
ment. Consequently, besides universal (do all computations
satisfy a property?) and existential (does some
computation satisfy a property?) questions, a third
question arises naturally: can the system resolve its
internal choices so that the satisfaction of a property
is guaranteed no matter how the environment resolves
the external choices? Such an alternating satisfaction
can be viewed as a winning condition in a two-player
game between the system and the environment. Alternation
is a natural generalization of existential and
universal branching, and has been studied extensively
in theoretical computer science [CKS81].
Different researchers have argued for game-like interpretations
of LTL and CTL specifications for open
systems. We list four such instances here. (1) Receptiveness
[Dil89, AL93, GSSL94]: given a reactive
system, specified by a set of safe computations (typ-
ically, generated by a transition relation) and a set
of live computations (typically, expressed by an LTL
formula), the receptiveness problem is to determine
whether every finite safe computation can be extended
to an infinite live computation irrespective of the behavior
the environment. It is sensible, and necessary
for compositionality, to require an affirmative answer
to the receptiveness problem. (2) Realizability (pro-
gram synthesis) [ALW89, PR89a, PR89b]: given an
sets of input and output signals,
the synthesis problem requires the construction of a
reactive system that assigns to every possible input sequence
an output sequence so that the resulting computation
satisfies /. (3) Supervisory control [RW89]:
given a finite-state machine whose transitions are partitioned
into controllable and uncontrollable, and a set
of safe states, the control problem requires the construction
of a controller that chooses the controllable
transitions so that the machine always stays within the
safe set (or satisfies some more general LTL formula).
Module checking [KV96]: given an open system
and a the module-checking problem
is to determine if, no matter how the environment restricts
the external choices, the system satisfies '.
All the above approaches use the temporal-logic
syntax that was developed for specifying closed sys-
tems, and reformulate its semantics for open systems.
In this paper, we propose, instead, to enrich temporal
logic so that alternating properties can be specified explicitly
within the logic: we introduce alternating-time
temporal logics for the specification and verification of
open systems. Our formulation of open systems con-
siders, instead of just a system and an environment,
the more general setting of a set \Sigma of agents that correspond
to different components of the system and the
environment. For the scheduling of agents, we consider
two policies. In each state of a synchronous sys-
tem, it is known in advance which agent proceeds. In
each state of an asynchronous system, several agents
may be enabled, and an unknown scheduler determines
which agent takes the next step. In the latter
case, the scheduler is required to be fair to each agent;
that is, in an infinite computation, an agent cannot be
continuously enabled without being scheduled.
For a set A ' \Sigma of agents, a set \Gamma of computations,
and a state w of the system, consider the following
game between a protagonist and an adversary. The
game starts at the state w. Whenever the scheduled
agent is in the set A, the protagonist chooses the next
state, and otherwise, the adversary chooses the next
state. If the resulting infinite computation belongs to
the set \Gamma, then the protagonist wins. If the protagonist
has a winning strategy, we say that the alternating-
time formula hhAii\Gamma is satisfied in the state w. Here,
hhAii is a path quantifier, parameterized with the set
A of agents, which ranges over all computations that
the agents in A can force the game into, irrespective
of how the agents in \Sigma nA play. Hence, the parameterized
path quantifier hhAii is a generalization of the path
quantifiers of branching-time temporal logics: the existential
path quantifier 9 corresponds to hh\Sigmaii, and the
universal path quantifier 8 corresponds to hh;ii. In par-
ticular, closed systems can be viewed as systems with
a single agent sys . Then, the two possible parameterized
path quantifiers hhsysii and hh;ii match exactly the
path quantifiers 9 and 8 required for specifying such
systems. Depending on the syntax used to specify the
set \Gamma of computations, we obtain two alternating-time
temporal logics: in the logic ATL ? , the set \Gamma is specified
by a formula of LTL; in the more restricted logic
ATL, the set \Gamma is specified by a single temporal operator
applied to a state formula. Thus, ATL is the
alternating generalization of CTL, and ATL ? is the
alternating generalization of CTL ? .
Alternating-time temporal logics can conveniently
express properties of open systems as illustrated by
the following five examples:
1. In a multi-process distributed system, we can require
any subset of processes to attain a goal,
irrespective of the behavior of the remaining
processes. Consider, for example, the cache-coherence
protocol for Gigamax verified using
SMV [McM93]. One of the desired properties
is the absence of deadlocks, where a deadlocked
state is one in which a processor, say a, is permanently
blocked from accessing a memory cell.
This requirement was specified using the CTL formul

The
captures the informal requirement more precisely.
While the CTL formula only asserts that it is always
possible for all processors to cooperate so
that a can eventually read and write ("collabora-
tive possibility"), the ATL formula is stronger: it
guarantees a memory access for processor a, no
matter what the other processors in the system do
("adversarial possibility").
2. While the CTL formula 82' asserts that the
state predicate ' is an invariant of a system component
irrespective of the behavior of all other
components ("adversarial invariance"), the ATL
(which stands for hh\Sigma n fagii 2')
states the weaker requirement that ' is a possible
invariant of the component a; that is, a cannot
violate 2' on its own, and therefore the other
system components may cooperate to achieve 2'
("collaborative invariance"). For ' to be an invariant
of a complex system, it is necessary (but
not sufficient) to check that every component a
satisfies the ATL formula [[a]]2'.
3. The receptiveness of a system whose live computations
are given by the LTL formula / is specified
by the
4. Checking the realizability (program synthesis) of
an corresponds to model checking
of the ATL ? formula hhsysii/ in a maximal model
that considers all possible inputs and outputs.
5. The controllability of a system whose safe states
are given by the state predicate ' is specified by
the
thesis, then, corresponds to model checking of this
formula. More generally, for an LTL formula /,
the ATL ? requirement hhcontrolii/ asserts that
the controller has a strategy to ensure the satisfaction
of /.
Notice that ATL is better suited for compositional reasoning
than CTL. For instance, if a component a satisfies
the CTL formula 93', we cannot conclude that
the compound system akb also satisfies 93'. On the
other hand, if a satisfies the ATL formula hhaii3',
then so does akb.
The model-checking problem for alternating-time
temporal logics requires the computation of winning
strategies. In the case of synchronous ATL, all
games are finite reachability games. Consequently,
the model-checking complexity is linear in the size of
the system and the length of the formula, just as in
the case of CTL. While checking existential reachability
corresponds to iterating the existential next-time
operator 9 , and checking universal reachability corresponds
to iterating the universal next 8 , checking
alternating reachability corresponds to iterating
an appropriate mix of 9 and 8 , as governed by a
parameterized path quantifier. This suggests a simple
model-checking procedure for synchronous
ATL, and shows how existing symbolic model checkers
for CTL can be modified to check ATL specifications,
at no extra cost. In the asynchronous model, due to
the presence of fairness constraints, ATL model checking
requires the solution of infinite games, namely,
generalized B-uchi games [VW86]. Consequently, the
model-checking complexity is quadratic in the size of
the system, and the symbolic algorithm involves a
nested fixed-point computation. The model-checking
problem for ATL ? is much harder: we show it to be
complete for 2EXPTIME in both the synchronous and
asynchronous cases.
2 The Alternating-time Logic ATL
2.1 Syntax
The temporal logic ATL (alternating-time logic) is defined
with respect to a finite set \Pi of propositions and
a finite set \Sigma of agents. An ATL formula is one of the
propositions
are ATL
formulas.
is a set of
agents, and are ATL formulas.
The operator hh ii is a path quantifier, and ("next")
and U ("until") are temporal operators. The logic
ATL is similar to the branching-time logic CTL, only
that path quantifiers are parameterized by sets of
agents. When ang is known, we write
an ii instead of hhfa an gii.
2.2 Synchronous-structure semantics
The formulas of ATL can be interpreted over a synchronous
structure
the set of propositions, \Sigma is the set of agents, W is a
set of states, R ' W \Theta W is a total transition relation
(i.e., for every state w 2 W there exists a state
such that R(w; w 0 )), the function -
maps each state w 2 W to the set -(w) ' \Pi of propositions
that are true in w, and the function oe
maps each state w 2 W to the agent oe(w) 2 \Sigma that is
enabled in w. Note that precisely one agent is enabled
in each state. For a set A ' \Sigma of agents, we denote
by WA ' W the set of states w for which oe(w) 2 A.
When fag is a singleton, we write W a instead
of W fag . For two states w and w 0 with R(w; w 0 ), we
say that w 0 is a successor of w. A computation of S is
an infinite sequence of states such
that for all i - 0, we have R(w We refer to a
computation starting at state w 0 as a w 0 -computation.
For a computation fl and an index i - 0, we use fl[i]
and fl[0; i] to denote the i-th state in fl and the finite
prefix of fl, respectively.
In order to define the semantics of ATL, we first define
the notion of strategies. A strategy for an agent
a 2 \Sigma is a function f a : W   \Delta W a ! W such that
if f a (fl \Delta
Thus, a strategy maps a finite prefix of
a computation to a possible extension of the compu-
tation. Intuitively, the strategy f a suggests for each
history fl and state w in which a is enabled, a successor
f a (fl \Delta w) of w. Each strategy f a induces a set
of computations that agent a can enforce. Given a
state w, a set ang of agents, and a set
an g of strategies for the agents in A,
we define the outcomes of FA from w to be the set
out(w; FA ) of all w-computations that the agents in A
can enforce when they cooperate and follow the strategies
in FA ; that is, a w-computation fl is in out (w; FA )
iff whenever fl visits a state whose agent is a k 2 A,
then the computation proceeds according to the strategy
f ak . Formally,
some a k 2 A, then w In particular,
then the outcome set out(w; FA ) contains a
single w-computation, and if A = ;, then the outcome
set out(w; FA ) contains all w-computations.
We can now turn to a formal definition of the semantics
of ATL. We write w to indicate that the
state w of the synchronous structure S satisfies the
(when the subscript S is clear from
the context, we omit it). The satisfaction relation
is defined, for all states w 2 W , inductively as follows:
ffl For p 2 \Pi, we have w
there exists a set FA of strate-
gies, one for each agent in A, such that for all
computations
there exists a set FA of strate-
gies, one for each agent in A, such that for all computations
there exists an index
we have fl[j]
train
train ctr
out of gate
in gate
request
out of gate
grant
out of gate
ctr

Figure

1: A synchronous train-controller system
Note that the next operator hhAii gives a local con-
straint: w there
exists a successor of w that satisfies ', or w 62 WA
and all successors of w satisfy '. For an
we denote by ['] ' W the set of states w
such that w
Since the parameterized path quantifiers hh\Sigmaii and
hh;ii correspond to existential and universal path quan-
tification, respectively, we write 9 for hh\Sigmaii and 8
for hh;ii. The logic CTL is the fragment of ATL
interpreted over structures with a single agent: if
8. As dual of
hh ii we use the path
quantifier hh\Sigma n Aii ranges over the computations that
the agents not in A have strategies to enforce, the path
quantifier ranges over the computations that the
agents in A do not have strategies to avoid. Therefore
also As in CTL, the temporal operators
3 ("eventually") and 2 ("always") are defined
from the until operator: hhAiitrue U' and
Example 2.1 Consider the synchronous structure
shown in Figure 1. The structure describes a protocol
for a train entering a gate at a railroad cross-
ing. At each moment, the train is either out of gate
or in gate. In order to enter the gate, the train issues
a request, which is serviced (granted or rejected)
by the controller in the next step. After a grant, the
train may enter the gate or relinquish the grant. The
structure has two agents: the train and the controller.
Two states of the structure, labeled ctr, are controlled;
that is, when a computation is in one of these states,
the controller chooses the next state. The other two
states are not controlled, and the train chooses successor
states. The system satisfies the following specifications

1. Whenever the train is outside the gate and does
not have a grant to enter the gate, the controller
can prevent it from entering the gate:
((out of gate -:grant) ! hhctr ii2out of gate)
2. Whenever the train is outside the gate, the controller
cannot force it to enter the gate:
(out of gate ! [[ctr]]2out of gate)
3. Whenever the train is outside the gate, the train
and the controller can cooperate so that the train
will enter the gate:
(out of gate ! hhctr ; trainii3in gate)
4. Whenever the train is in the gate, the controller
can force it out in a single step:
out of gate)
The first two specifications cannot be stated in CTL or
They provide more information than the CTL
out of gate).
While ' only requires the existence of a computation
in which the train is always outside the gate, the ATL
formulas guarantee that no matter how the train be-
haves, the controller can prevent it from entering the
gate, and no matter how the controller behaves, the
train can decide to stay outside the gate. Since all the
states of the structure are either controller states or
train states, the third specification is equivalent to the
(out of gate ! 93 in gate).
2.3 Asynchronous-structure semantics
The formulas of ATL can also be interpreted over an
asynchronous structure
\Pi, \Sigma, R, and L are as in a synchronous structure, and
the function oe maps each transition r 2 R to
the agent oe(r) 2 \Sigma that owns r. For an agent a 2 \Sigma,
we denote by R a ' R the set of transitions owned
by a. For two states w and w 0 with R a (w; w 0 ), we say
that w 0 is an a-successor of w. Note that a state w
may have none or several a-successors. For a state w,
we define enabled (w) ' \Sigma to be the set of agents a
for which there exists an a-successor of w. We write
W a for the set of states w with a 2 enabled(w). As
for synchronous structures, a computation of S is an
infinite sequence of states such that
for all i - 0, we have R(w Given a set A ' \Sigma
of agents, the computation fl is A-fair iff for each agent
a 2 A and each index i - 0, there exists a j - i
such that either a 62 enabled (w j ) or R a (w
is, in an A-fair computation, no agent in A can be
continuously enabled without being scheduled. 1
Similar to the synchronous case, a strategy for an
agent a 2 \Sigma is a function f a : W   \Delta W a ! W such
that if f a (fl \Delta
then R a (w; w 0 ). Thus, the agent a applies its strategy
and influences the computation whenever it is
scheduled. However, unlike in synchronous structures,
it is not known in advance which agent is scheduled
when a particular state is encountered. Given
a state w, a set ang of agents, and a set
an g of strategies for the agents in A,
we define the outcomes out (w; FA ) to be the set of
all w-computations that the agents in A can enforce
when they follow the strategies f f an and the
scheduling policy is fair with respect to A. Formally,
the computation
for some a k 2 A, then w
is A-fair. The definition of satisfaction of ATL formulas
in an asynchronous structure is the same as in
the synchronous case, with the above definition of out-
comes. For example, w for every agent
a 2 enabled (w), either a 2 A and there exists an a-
successor w 0 of w such that w 0 or a 62 A and for
all a-successors w 0 of w, we have w 0 synchronous
ATL is the fragment of asynchronous ATL
interpreted over structures where for each state w, the
set enabled(w) of enabled agents is a singleton. If the
set \Sigma of agents is a singleton, then the synchronous
and asynchronous interpretations coincide (and are
equal to CTL).
Example 2.2 Consider the asynchronous structure
shown in Figure 2. The structure again describes a
Our algorithms can be easily modified to account for differ-
ent, stronger types of fairness.
out of gate
in gate
request
out of gate
grant
out of gate
train
ctr
train
train
train train
ctr
ctr ctr

Figure

2: An asynchronous train-controller system
protocol for a train entering a gate. The protocol is
similar to the one described in Example 2.1, only that
requests by the train to enter the gate are serviced
asynchronously, at some future step. A fair scheduling
policy ensures that each request will be serviced
(granted or rejected) eventually. All four specifications
from Example 2.1 hold also for the asynchronous
system.
Checking
The synchronous (resp. asynchronous) model-checking
problem for ATL asks, given a synchronous (asyn-
chronous) structure S and an ATL formula ', for
the set ['] of states of S that satisfy '. We measure
the complexity of the model-checking problem in
two ways: the joint complexity of model checking considers
the complexity in terms of both the size of the
structure and the length of the formula; the structure
complexity of model checking considers the complexity
in terms of the structure only, assuming the formula
is fixed. Since the structure is typically much larger
than the formula, and its size is the most common
computational bottle-neck, the structure-complexity
measure is of particular practical interest [LP85].
3.1 The synchronous model
Model checking for synchronous ATL is very similar
to CTL model checking [CE81, QS81, BCM
first present a symbolic algorithm, which manipulates
state sets of the given synchronous structure S. The
algorithm is shown in Figure 3, and uses the following
primitive operations:
ffl The function Sub, when given an
returns a queue Sub(') of subformulas of ' such
that if ' 1 is a subformula of ' and ' 2 is a sub-formula
of ' 1 , then ' 2 precedes ' 1 in the queue
Sub(').
ffl The function PropCheck , when given a proposition
returns the state set [p].
ffl The function Pre, when given two state sets ae
and - , returns the set of states w such that either
some successor of w is in - , or w 62 ae
and all successors of w are in - .
ffl Union, intersection, difference, and inclusion test
for state sets.
These primitives can be implemented using symbolic
representations, such as binary decision diagrams, for
state sets and the transition relation. If given a symbolic
model checker for CTL, such as SMV [McM93],
only the Pre operation needs to be modified for checking
ATL.
for each ' 0 in Sub(') do
case
case
case
case
case
ae := [false]; - := [' 2 ];
while - 6' ae do
ae
case
return ['].

Figure

3: Symbolic ATL model checking
Alternatively, the ATL model-checking algorithm
can be implemented using an enumerative representation
for the state set W of the structure S. Then,
for each subformula ' 0 of ', every state w 2 W is
labeled with ' 0 iff w 2 [' 0 ], and w is labeled with
The labeling of the states with formulas
proceeds in a bottom-up fashion, following the
ordering Sub(') from smaller to larger subformulas.
If ' 0 is generated by the rules (S1) or (S2) or has
the form hhAii ', the labeling procedure is straight-
forward. For the labeling procedure
corresponds to solving a reachability problem for
an AND-OR graph: the states in WA are OR-nodes,
the remaining states are AND-nodes, and we need to
compute the set of nodes from which the OR-player
can reach a state labeled by ' 2 while staying within
states labeled by ' 1 . Since the reachability problem for
AND-OR graphs can be solved in time linear in the
number of edges, it follows that the labeling procedure
requires linear time for each subformula. Furthermore,
since reachability for AND-OR graphs, a PTIME-hard
problem [Imm81], can be reduced to model checking
for synchronous ATL, we conclude the following theorem

Theorem 3.1 The synchronous model-checking problem
for ATL is PTIME-complete, and can be solved in
time O(m') for a structure with m transitions and an
formula of length '. The structure complexity of
the problem is also PTIME-complete.
It is interesting to compare the model-checking complexities
of synchronous ATL and CTL. While both
problems can be solved in time O(m') [CES86], the
structure complexity of CTL model checking is only
NLOGSPACE-complete [BVW94]. This is because
model checking is related to graph reachabil-
ity, as synchronous ATL model checking is related to
AND-OR graph reachability.
3.2 The asynchronous model
Consider an asynchronous structure S with the state
set W , and a formula ' of ATL. As in the synchronous
case, for each subformula ' 0 of ', we compute the set
of states that satisfy ' 0 , starting from the inner-most
subformulas. For this purpose, we transform the
asynchronous structure S into a synchronous structure
S 0 as follows. The propositions of S 0 are the propositions
of S. The agents of S 0 are the agents of S,
plus a new agent b called scheduler. The states of S 0
are the states of S, plus for every state w 2 W and
every agent a enabled in w, a new state q w;a . Then,
each transition of S from w to w 0 owned by agent a
is replaced in S 0 by two transitions, one from w to
q w;a and the other from q w;a to w 0 . The propositions
that are true in the states w and q w;a of S 0 are those
that are true in the state w of S. The agent that is
enabled in the state w of S 0 is b, and the agent that
is enabled in the state q w;a of S 0 is a. Thus, in the
synchronous structure, first the scheduler chooses one
of the enabled agents, and then the chosen agent takes
a step.
Consider the subformula hhaii3' of ' (more general
until formulas can be handled similarly). The evaluation
of this formula in a state w 0 2 W corresponds to
the following game between a protagonist and an ad-
versary. The game is played on the synchronous structure
starting from w 0 . When the agent enabled in
the current state is a, the protagonist chooses a successor
state in S 0 ; otherwise the adversary chooses the
next state. When a state in W satisfying ' is visited,
the protagonist wins. If the game continues forever,
then the adversary wins iff the resulting computation
is fair to the agent a; that is, it contains either infinitely
many states of the form q w;a or infinitely many
states w 2 W such that a is not enabled in the state w
of S. Then, the state w 0 satisfies the formula hhaii3'
in S iff the protagonist has a winning strategy. The
winning condition of the adversary can be specified
by the
a -:W a )), where W a
defines the states of S in which a is enabled and W 0
a
defines the states of S 0 in which a is enabled. This is
a B-uchi game, and the set of winning states for the
adversary can be computed by a nested fixed-point
computation:
ae := [true]; - := [:'];
while ae 6' - do
ae
a [ (W n W a
while - 6' ae 0 do
a
od
od.
In an enumerative implementation, the complexity of
solving a B-uchi game is quadratic in the number of
transitions of a structure [VW86]. If S has m transi-
tions, then S 0 has 2m transitions. Thus, the labeling
procedure for the subformula hhaii3' requires O(m 2 )
time.
For the subformula ' an ii3', the
winning condition of the adversary is a conjunction
of n B-uchi conditions (to be precise, 2(:' -
ak -:W ak )). Such a game can be transformed
into a game with a single B-uchi condition by
introducing a counter variable that ranges over the
set ng [VW86]. Hence, the labeling procedure
for the subformula ' 0 requires O(m 2 To determine
the complexity of evaluating all subformulas
of ', we define the size of a logical connective to be 1,
and the size of a temporal connective to be the number
of agents in the corresponding path quantifier. Then,
are the sizes of all connectives in ', the
time complexity is O(m 2 n 2
k ), or
bounded by the
length ' of the formula '. Finally, since the synchronous
model-checking problem is a special case of
the asynchronous problem, we conclude the following
theorem.
Theorem 3.2 The asynchronous model-checking
problem for ATL is PTIME-complete, and can be
solved in time O(m 2 ' 2 ) for a structure with m transitions
and an ATL formula of length '. The structure
complexity of the problem is also PTIME-complete.
It is interesting to compare the model-checking complexities
of asynchronous ATL and Fair-CTL, with
generalized B-uchi fairness constraints. While the latter
is can be solved in O(mk') time [VW86], where
k is the number of B-uchi constraints, the best known
algorithm for the former is quadratic in m. This is because
model checking is related to checking
the emptiness of B-uchi automata, and asynchronous
model checking is related to checking the emptiness
of alternating B-uchi automata.
4 The Alternating-time Logic ATL ?
The logic ATL is a fragment of a more expressive logic
called . There are two types of formulas in
state formulas, whose satisfaction is related to a specific
state, and path formulas, whose satisfaction is
related to a specific computation. Formally, a state
formula is one of the following:
propositions
are state
formulas.
hhAii/, where A ' \Sigma is a set of agents, and / is
a path formula.
path formula is one of the following:
are path
formulas.
are path
formulas.
The logic ATL ? consists of the set of state formulas
generated by the above rules. It is similar to the
branching-time temporal logic CTL ? , only that path
quantifiers are parameterized by sets of agents. The
logic ATL is the fragment of ATL ? that consists of all
formulas in which every temporal operator is immediately
preceded by a path quantifier.
The semantics of ATL ? is defined similarly to the
semantics for ATL. We write fl to indicate that
the computation fl of the structure S satisfies the path
(the subscript S is usually omitted). The
satisfaction relation j= is defined, for all states w and
computations fl, inductively as follows:
ffl For state formulas generated by the rules (S1) and
(S2), the definition of j= is the same as for ATL.
there exists a set FA of strategies,
one for each agent in A, such that for all computations
for a state formula ' iff fl[0]
there exists an index i - 0 such
that fl[i]
As before,
The temporal operators 3 and 2 are defined from
U as usual:
For example, the
asserts that agent a has a strategy to enforce
that, whenever a request is continuously issued,
infinitely many grants are given. This specification
cannot be expressed in CTL ? or in ATL. For single-agent
structures, degenerates to CTL ? .
While there is an exponential price to be paid in
model-checking complexity when moving from CTL to
price becomes even more significant when
we consider the alternating-time versions of the logics.
Theorem 4.1 In both the synchronous and asynchronous
cases, the model-checking problem for ATL ?
is 2EXPTIME-complete. In both cases, the structure
complexity of the problem is PTIME-complete.
Proof (sketch). Given a synchronous structure S with
state set W , and an ATL ? formula ', we label the
states in S with state subformulas of ', starting from
the innermost state subformulas. For state subformulas
of the form hhAii/, we employ the algorithm
module checking from [KV96] as follows.
Let / 0 the result of replacing in / all state subfor-
mulas, which have already been evaluated, by appropriate
new propositions. For a state w and a set FA of
strategies, the set out(w; FA ) of computations induces
a tree, which is obtained by unwinding S from w and
then pruning all subtrees whose roots are successors
of states in WA that are not chosen by the strategies
in FA . We construct a B-uchi tree automaton Tw;A
that accepts all trees induced by out(w; FA ) for any
set FA of strategies, and a Rabin tree automaton T/
that accepts all trees satisfying the
By [KV96], Tw;A has jW j states. By [ES84], T/ has
states and 2 O(j/j) acceptance pairs. The intersection
of the two automata is a Rabin tree automaton
that contains the outcome trees satisfying 8/ 0 . Hence,
by the semantics of ATL ? , the state w satisfies hhAii/
iff this intersection is nonempty. By [EJ88, PR89a],
the nonemptiness problem for a Rabin tree automaton
with n states and k pairs can be solved in time
O(kn) 3n . Hence, evaluating the subformula hhAii/ in
a single state requires at most time
. Since
there are jW j states and O(j'j) many subformulas,
membership in 2EXPTIME follows.
The asynchronous case can be reduced to the synchronous
case similar to the proof of Theorem 3.2.
For the lower bounds, we use a reduction from the realizability
problem of LTL, a 2EXPTIME-hard problem
[Ros92], to model checking for synchronous ATL ? .
By contrast, CTL ? model checking is only PSPACE-complete
[CES86], and its structure complexity is
NLOGSPACE-complete [BVW94].
The verification problem for open systems, more than
it corresponds to the model-checking problem for temporal
logics, corresponds, in the case of linear time,
to the realizability problem [ALW89, PR89a, PR89b],
and in the case of branching time, to the module-
checking problem [KV96]; that is, to a search for winning
strategies of !-regular games. In general, this
involves a hefty computational price. The logic ATL
identifies an interesting class of properties that can be
checked by solving finite games, which demonstrates
that there is still a great deal of reasoning about open
systems that can be performed efficiently. We conclude
with several remarks on variations of ATL which
support our design choices.
5.1 Agents with limited memory
In the definitions of ATL and ATL ? , the strategy of an
agent may depend on an unbounded amount of infor-
mation, namely, the full history of the game up to the
current state. However, since all involved games are !-
regular, the existence of a winning strategy implies the
existence of a winning finite-state strategy [Tho95],
which depends only on a finite amount of information
about the history of the game. Thus, the semantics
of ATL and ATL ? can be defined, equivalently, using
the outcomes of finite-state strategies only. This is in-
teresting, because a strategy can be thought of as the
parallel composition of the system with a controller,
which makes sure that the system follows the strat-
egy. Then, for an appropriate definition of parallel
composition, it is precisely the finite-state strategies
that can be implemented using controllers that are
synchronous structures. Indeed, for the finite reachability
games and generalized B-uchi games of ATL,
it suffices to consider memory-free strategies [Tho95],
which can be implemented as control maps (i.e., controllers
without state). This is not the case for ATL ? ,
whose formulas can specify the winning positions of
games [Tho95].
5.2 Agents with limited information
Our models assume that the agents of a structure have
complete information about all propositions (which
state satisfies which propositions) and about the other
agents (which agent owns which transitions). Sometimes
it may be more appropriate to assume that each
agent a 2 \Sigma can observe only a subset \Pi a ' \Pi of
the propositions, and a strategy f a : \Pi
a ! \Pi a for a
must (1) depend only on the observable part of the
history and (2) decide only on the observable part of
the next state. From undecidability results on multi-player
games with incomplete information, it follows
that the model-checking problem for ATL with incomplete
information is undecidable in both the synchronous
[Yan97] and asynchronous [PR79] cases. In
the special case that all path quantifiers are parameterized
by single agents, and no cooperation between
agents with different information is possible, decidability
follows from the results on module checking
with incomplete information [KV97]. In this case,
the model-checking complexity for both synchronous
and asynchronous ATL is EXPTIME-complete, and
2EXPTIME-complete for ATL ? . The structure complexity
of all four problems is EXPTIME-complete,
thus rendering reasoning about agents with incomplete
information infeasible even under severe restrictions

5.3 Game logic and module checking
The parameterized path quantifier hhAii first stipulates
the existence of strategies for the agents in A and then
universally quantifies over the outcomes of the stipulated
strategies. One may generalize ATL and ATL ?
by separating the two concerns into strategy quantifiers
and path quantifiers, say, by writing 99A: 8 instead
of hhAii (read 99A as "there exist strategies for
the agents in A"). Then, for example, the formula
asserts that the agents in
A have strategies such that for some behavior of the
remaining agents, ' 1 is always true, and for some possibly
different behavior of the remaining agents, ' 2 is
always true. To define the semantics of strategy quan-
tifiers, we need to consider the tree that is induced by
the outcomes of a set of strategies, and obtain three
types of formulas: state formulas and path formulas
as in CTL ? or ATL ? , and tree formulas, whose satisfaction
is related to a specific outcome tree. For
instance, while ' is a state formula, its subformula
is a tree formula. We refer to the general
logic with strategy quantifiers, path quantifiers,
temporal operators, and boolean connectives as game
logic. Then, ATL ? is the fragment of game logic that
consists of all formulas in which every strategy quantifier
is immediately followed by a path quantifier (note
that 99A: 9 is equivalent to 9).
Another fragment of game logic is studied in module
checking [KV96]. There, one considers formulas of
the form 99A: ', with a single outermost strategy quantifier
followed by a CTL or CTL ? formula '. From
an expressiveness viewpoint, alternating-time logics
and module checking identify incomparable fragments
of game logic: the formula ' from above is not
equivalent to any ATL ? formula, and the ATL formula
not equivalent to any formula
with a single strategy quantifier. In [KV96],
it is shown that the module-checking complexity
is EXPTIME-complete for CTL and 2EXPTIME-
complete for CTL ? , and the structure complexity of
both problems is PTIME-complete. Applying the
method there in a bottom-up fashion can be used
to solve the model-checking problem for game logic,
resulting in a joint complexity of 2EXPTIME and a
structure complexity of PTIME. Thus, game logic is
no more expensive than ATL ? . We feel, however, that
unlike state and path formulas, tree formulas are not
natural specifications of reactive systems.
5.4 Alternating-time fixpoint logic
Temporal properties using the until operator can be
defined as fixed points of next-time properties. For
closed systems, this gives the -calculus as a generalization
of temporal logics [Koz83]. In a similar fashion,
one can generalize alternating-time temporal logics to
obtain an alternating-time -calculus, whose primitives
are the parameterized next constructs hhAii and
least and greatest fixed-point operators, and
positive boolean connectives. Then, ATL ? is a proper
fragment of the alternating-time -calculus, and every
formula is equivalent to a fixed-point formula
without alternation of least and greatest fixed
points. In practice, however, designers prefer temporal
operators over fixed points [BBG just as
CTL and CTL ? capture useful and friendly subsets of
the -calculus for the specification of closed system,
ATL and ATL ? capture useful and friendly subsets
of the alternating-time -calculus for the specification
of open systems. It is worth noting that CTL with
parameterized next constructs is not of sufficient use,
because it cannot specify the unbounded alternating
reachability property hhAii3' [BVW94]. Hence it is
essential that in ATL we can parameterize path quan-
tifiers, not just next-time operators.
Alternating-time transition systems
The parameterized next construct hhAii is different
from similar operators commonly written as 9 A and
interpreted as "for some agent a 2 A, there exists
an a-successor." Rather, the ATL formula hhAii ' is
equivalent to 9 A' - 8 \SigmanA '. For the abstract specification
of open systems, it is essential that the parameterized
next has a game-like interpretation, not a
standard modal interpretation. This is because our
definitions of synchronous and asynchronous structures
are only approximations of "real" concurrency
models for open systems (synchronous, e.g. [AH96],
or asynchronous, e.g. [Lyn96]). While in our struc-
tures, each transition corresponds to a step of a single
agent, in these models, a transition may be the result
of simultaneous independent decisions by several
agents. The more general situation gives rise to games
with complex individual moves that can be captured
abstractly by alternating transition systems (see the
full paper). The game-like interpretation of the parameterized
next makes ATL robust with respect to
such changes in the definition of individual moves. In
particular, all of our results carry over to alternating
transition systems, and therefore apply, for example,
to Reactive Modules [AH96].

Acknowledgments

. We thank Amir Pnueli, Moshe
Vardi, and Mihalis Yannakakis for helpful discussions.



--R

Reactive modules.
Composing specifica- tions
Realizable and unrealizable concurrent program specifications.

Symbolic model checking: 10 20 states and beyond.
An automata-theoretic approach to branching-time model checking
Design and synthesis of synchronization skeletons using branching-time temporal logic
Automatic verification of finite-state concurrent systems using temporal logic specifications

Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits
on branching versus linear time.
The complexity of tree automata and logics of programs.
Deciding branching-time logic
Liveness in timed and untimed systems.
Communicating Sequential Pro- cesses
The model checker SPIN.
Number of quantifiers is better than number of tape cells.
Results on the propositional - calculus
Module checking.
Module checking re- visited
Checking that finite-state concurrent programs satisfy their linear specification
Distributed Algorithms.
Symbolic Model Checking.
The temporal logic of programs.

On the synthesis of a reactive module.
On the synthesis of an asynchronous reactive module.
Specification and verification of concurrent systems in Cesar.
The control of discrete event systems.
Modular Synthesis of Reactive Sys- tems
On the synthesis of strategies in infinite games.

Personal communication
--TR
Communicating sequential processes
MYAMPERSANDldquo;SometimesMYAMPERSANDrdquo; and MYAMPERSANDldquo;not neverMYAMPERSANDrdquo; revisited
Automatic verification of finite-state concurrent systems using temporal logic specifications
On the synthesis of a reactive module
Trace theory for automatic hierarchical verification of speed-independent circuits
Automata on infinite objects
Temporal and modal logic
Symbolic Boolean manipulation with ordered binary-decision diagrams
Symbolic model checking
and ECTL as fragments of the modal MYAMPERSANDmgr;-calculus
Conjoining specifications
The Model Checker SPIN
Modalities for model checking (extended abstract)
Checking that finite state concurrent programs satisfy their linear specification
On the menbership problem for functional and multivalued dependencies in relational databases
Alternation
Reactive Modules
An automata-theoretic approach to branching-time model checking
Module checking
JMOCHA
Distributed Algorithms
Symbolic Model Checking
Automata on Infinite Objects and Church''s Problem
Realizable and Unrealizable Specifications of Reactive Systems
On the Synthesis of an Asynchronous Reactive Module
Fair Simulation Relations, Parity Games, and State Space Reduction for BMYAMPERSANDuuml;chi Automata
Small Progress Measures for Solving Parity Games
The Control of Synchronous Systems
The Control of Synchronous Systems, Part II
On the Complexity of Branching Modular Model Checking (Extended Abstract)
Specification and verification of concurrent systems in CESAR
MOCHA
A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal Mu-Calculus
Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic
Liveness in Timed and Untimed Systems
Trees, automata, and games
Deciding branching time logic

--CTR
Xianwei Lai , Shanli Hu , Zhengyuan Ning, An Improved Formal Framework of Actions, Individual Intention and Group Intention for Multi-agent Systems, Proceedings of the IEEE/WIC/ACM international conference on Intelligent Agent Technology, p.420-423, December 18-22, 2006
Wojciech Jamroga , Thomas gotnes, What agents can achieve under incomplete information, Proceedings of the fifth international joint conference on Autonomous agents and multiagent systems, May 08-12, 2006, Hakodate, Japan
Thomas gotnes , Wiebe van der Hoek , Michael Wooldridge, On the logic of coalitional games, Proceedings of the fifth international joint conference on Autonomous agents and multiagent systems, May 08-12, 2006, Hakodate, Japan
Suchismita Roy , Sayantan Das , Prasenjit Basu , Pallab Dasgupta , P. P. Chakrabarti, SAT based solutions for consistency problems in formal property specifications for open systems, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.885-888, November 06-10, 2005, San Jose, CA
Luigi Sauro , Jelle Gerbrandy , Wiebe van der Hoek , Michael Wooldridge, Reasoning about action and cooperation, Proceedings of the fifth international joint conference on Autonomous agents and multiagent systems, May 08-12, 2006, Hakodate, Japan
Krishnendu Chatterjee , Luca de Alfaro , Thomas A. Henzinger, The complexity of quantitative concurrent parity games, Proceedings of the seventeenth annual ACM-SIAM symposium on Discrete algorithm, p.678-687, January 22-26, 2006, Miami, Florida
van der Hoek , Michael Wooldridge, On the dynamics of delegation, cooperation, and control: a logical account, Proceedings of the fourth international joint conference on Autonomous agents and multiagent systems, July 25-29, 2005, The Netherlands
Aleksandra Nenadi , Ning Zhang , Qi Shi, RSA-based verifiable and recoverable encryption of signatures and its application in certified e-mail delivery, Journal of Computer Security, v.13 n.5, p.757-777, October 2005
Aldewereld , Wiebe van der Hoek , John-Jules Meyer, Rational Teams: Logical Aspects of Multi-Agent Systems, Fundamenta Informaticae, v.63 n.2-3, p.159-183, April 2004
Valentin Goranko , Govert van Drimmelen, Complete axiomatization and decidability of alternating-time temporal logic, Theoretical Computer Science, v.353 n.1, p.93-117, 14 March 2006
Thomas A. Henzinger, Games in system design and verification, Proceedings of the 10th conference on Theoretical aspects of rationality and knowledge, June 10-12, 2005, Singapore
van der Hoek , Alessio Lomuscio , Michael Wooldridge, On the complexity of practical ATL model checking, Proceedings of the fifth international joint conference on Autonomous agents and multiagent systems, May 08-12, 2006, Hakodate, Japan
van der Hoek , Mark Roberts , Michael Wooldridge, Knowledge and social laws, Proceedings of the fourth international joint conference on Autonomous agents and multiagent systems, July 25-29, 2005, The Netherlands
Alur , Pavol ern , P. Madhusudan , Wonhong Nam, Synthesis of interface specifications for Java classes, ACM SIGPLAN Notices, v.40 n.1, p.98-109, January 2005
van der Hoek , Wojciech Jamroga , Michael Wooldridge, A logic for strategic reasoning, Proceedings of the fourth international joint conference on Autonomous agents and multiagent systems, July 25-29, 2005, The Netherlands
Krishnendu Chatterjee , Thomas A. Henzinger , Marcin Jurdziski, Games with secure equilibria, Theoretical Computer Science, v.365 n.1, p.67-82, 10 November 2006
Alessio Lomuscio , Franco Raimondi, Model checking knowledge, strategies, and games in multi-agent systems, Proceedings of the fifth international joint conference on Autonomous agents and multiagent systems, May 08-12, 2006, Hakodate, Japan
Alur , Salvatore La Torre , P. Madhusudan, Modular strategies for recursive game graphs, Theoretical Computer Science, v.354 n.2, p.230-249, 28 March 2006
Wojciech Jamroga , Wiebe van der Hoek, Agents that Know How to Play, Fundamenta Informaticae, v.63 n.2-3, p.185-219, April 2004
Magdalena Kacprzak , Wojciech Penczek, Fully Symbolic Unbounded Model Checking for Alternating-time Temporal Logic1, Autonomous Agents and Multi-Agent Systems, v.11 n.1, p.69-89, July      2005
van der Hoek , Michael Wooldridge, On the logic of cooperation and propositional control, Artificial Intelligence, v.164 n.1-2, p.81-119, May 2005
Yves Bontemps , Pierre-Yves Schobbens , Christof Lding, Synthesis of Open Reactive Systems from Scenario-Based Specifications, Fundamenta Informaticae, v.62 n.2, p.139-169, April 2004
D. R. Ghica , A. S. Murawski , C.-H. L. Ong, Syntactic control of concurrency, Theoretical Computer Science, v.350 n.2, p.234-251, 7 February 2006
van der Hoek, Knowledge, Rationality and Action, Proceedings of the Third International Joint Conference on Autonomous Agents and Multiagent Systems, p.16-23, July 19-23, 2004, New York, New York
games;temporaxl logic;alternation;model checking