=Paper=
{{Paper
|id=Vol-223/paper-2
|storemode=property
|title=Model Checking Abilities under Incomplete Information Is Indeed Delta2-complete
|pdfUrl=https://ceur-ws.org/Vol-223/66.pdf
|volume=Vol-223
|authors=Wojtek Jamroga (Clausthal University of Technology),Juergen Dix (Clausthal University of Technology)
|dblpUrl=https://dblp.org/rec/conf/eumas/JamrogaD06
}}
==Model Checking Abilities under Incomplete Information Is Indeed Delta2-complete==
https://ceur-ws.org/Vol-223/66.pdf
Model Checking Abilities under Incomplete Information
Is Indeed ∆P
2 -complete
Wojciech Jamroga Jürgen Dix
Department of Informatics,
Clausthal University of Technology, Germany
{wjamroga,dix}@in.tu-clausthal.de
Abstract
We study the model checking complexity of Alternating-time temporal logic with imperfect
information and imperfect recall ( atlir ). Contrary to what we have stated in [11], the problem
turns out to be ∆P 2 -complete, thus con rming the initial intuition of Schobbens [18]. We prove
∆P 2 -hardness through a reduction of the SNSAT problem, while the membership in ∆2 stems
P
from the algorithm presented in [18].
Keywords: multi-agent systems, model checking, temporal logic, strategic ability, computa-
tional complexity.
1 Introduction
Alternating-time temporal logic [1, 2] is one of the most interesting frameworks that emerged re-
cently for reasoning about computational systems. Atlir is a variant ofatl , proposed by Schobbens
in [18] for agents with imperfect information and imperfect recall. We have already investigated
the complexity of atl ir model checking in [11], concluding that the problem is NP-complete.
Unfortunately, our claim was incorrect; we set it right with this paper.
We begin with a presentation of the frameworks of atl and atl ir . Then we present some
existing complexity results with respect to atlir model checking, and we give an alternative proof
of NP-hardness of the problem. In Section 3.2, we extend the construction to present a reduction
of SNSAT, thus proving that model checking atl
ir is ∆2 -hard. As the membership in ∆2
P P
stems from the algorithms presented in both [18] and [11], we get that model checking atl ir is
∆P -complete.
Atl atl
2
ir can be seen as the core, minimal -based language for ability under incomplete infor-
mation: it does not contain any super uous formulae or operators. This is no formal statement
other researchers might come up with a weaker language that they consider appropriate. Neverthe-
less, atl ir is subsumed by the majority of existing logics that combine strategies and qualitative
uncertainty. By proving ∆P 2 -completeness of atl ir model checking, we obtain a lower bound for
model checking of virtually all logics of this kind, and for most of them the bound is tight.
2 What Agents Can Achieve
Atl [1, 2] has been invented by Alur, Henzinger and Kupferman in order to capture properties
of open computational systems (such as computer networks), where dierent components can act
autonomously, and computations in such systems result from their combined actions. Alternatively,
atl can serve as a logic for systems involving multiple agents, that allows one to reason about what
agents can achieve in game-like scenarios. As atl
does not include incomplete information in its
scope, it can be seen as a logic for reasoning about agents who always have complete knowledge
about the current state of aairs.
2.1 ATL: Ability in Perfect Information Games
Atl is a generalization of the branching time temporal logic ctl
[4, 5], in which path quanti ers
are replaced with so called cooperation modalities. Formula hhAiiϕ, where A ⊆ Agt is a coalition of
agents (Agt is the set of all agents), expresses that coalition A has a collective strategy to enforce ϕ.
Atl formulae include temporal operators: g (in the next state), (always from now on) and
U (until). Operator ♦ (now or sometime in the future) can be de ned as ♦ϕ ≡ > U ϕ. Like in
ctl , every occurrence of a temporal operator is immediately preceded by exactly one cooperation
modality.1 The broader language of atl
∗
, in which no such restriction is imposed, is not used in
this paper.
A number of semantics have been de ned for atl
, most of them equivalent [6, 7]. In this paper,
we refer to a variant of concurrent game structures, which includes a nonempty nite set of all
agents Agt = {1, ..., k}, a nonempty set of states St, a set of atomic propositions Π, a valuation of
propositions π : Π → P(St), and the set of (atomic) actions Act. Function d : Agt × St → P(Act)
de nes nonempty sets of actions available to agents at each state, and o is a (deterministic) transition
function that assigns the outcome state q 0 = o(q, α1 , . . . , αk ) to state q and a tuple of actions
hα1 , . . . , αk i that can be executed by the agent in q . A strategy sa of agent a is a conditional
plan that speci es what a is going to do for every possible state (i.e., sa : St → Act such that
sa (q) ∈ da (q)).2 A collective strategy SA for a group of agents A ⊆ Agt is a tuple of strategies, one
per agent from A. A path λ in model M is an in nite sequence of states that can be reached by
subsequent transitions, and refers to a possible course of action (or a possible computation) that
may occur in the system; by λ[i], we denote the ith position on path λ. Function out(q, SA ) returns
the set of all paths that may result from agents A executing strategy SA from state q onward. Now,
informally speaking, M, q |= hhAiiϕ i there is a collective strategy SA such that ϕ holds for every
λ ∈ out(q, SA ). In Section 2.3, we give a more precise semantic de nition of atl
ir , which is the
main subject of our study.
One of the most appreciated features of atl
is its model checking complexity linear in the
number of transitions in the model and the length of the formula. However, after a careful inspec-
tion, this result is not as good as it seems. This linear complexity is no more valid when we measure
the size of models in the number of states, actions and agents [10, 16], or when we represent systems
in a more compact way [19]. Still, we have the following.
Proposition 1 ([2]) The atl model checking problem is ptime-complete, and can be done in time
O(ml), where m is the number of transitions in the model and l is the length of the formula.
2.2 Strategic Abilities under Incomplete Information
Atl and its models include no way of addressing uncertainty that an agent or a process may have
about the current situation. Moreover, strategies in atl can de ne dierent choices for any pair
of dierent states, hence implying that an agent can recognize each (global) state of the system,
and act accordingly. Thus, it can be argued that the logic is tailored for describing and analyzing
systems in which every agent/process has complete and accurate knowledge about the current state
of the system. This is usually not the case for most application domains, where a process can
access its local state, but the state of the environment and the (local) states of other agents can be
observed only partially.
One of the main challenges for a logic of strategic abilities under incomplete information is the
question of how agents' knowledge should interfere with the agents' available strategies. The early
approaches to atl with incomplete information [2, Sec.7.2],[20, 21] did not handle this interac-
tion in a completely satisfactory way (cf. [9, 18, 15]), which triggered a urry of logics, proposed
to overcome the problems [9, 12, 18, 15, 22, 8, 13]. Most of the proposals agree that only uniform
strategies (i.e., strategies that specify the same choices in indistinguishable states) are really exe-
cutable. However, in order to identify a successful strategy, the agents must consider not only the
courses of actions starting from the current state of the system, but also those starting from states
that are indistinguishable from the current one. There are many cases here, especially when group
1 The logic to which such a syntactic restriction applies is sometimes called vanilla atl (resp. vanilla ctl etc.).
2 Note that in the original formulation of atl [1, 2], strategies assign agents' choices to sequences of states, which
suggests that agents can by de nition recall the whole history of each game.
epistemics is concerned: the agents may have common, mutual or distributed knowledge about
a strategy being successful, or they may be given a hint for the right strategy by a distinguished
member (the boss), a subgroup (headquarters committee) or even another group of agents (con-
sulting company) etc. Most existing solutions treat only some of the cases (albeit rather in an
elegant way), while the others oer a very general treatment of the problem at the expense of
a complicated logical language (which is by no means elegant). We believe that an elegant and
general solution has been recently proposed in the form of Constructive Strategic Logic [13, 14],
but this claim is yet to be veri ed.
Atl ir stands out among the existing solutions for its simplicity. While by no means the most
expressive, we believe it can be treated as the core, minimal atl
-based language for ability under
incomplete information. This is no formal statement; we just cannot think of a substantially weaker
temporal language to express abilities of agents.
2.3 ATLir
Atl ir includes the same formulae as atl
, only the cooperation modalities are presented with a
subscript: hhAiiir to indicate that they address agents with imperfect information and imperfect
recall. Formally, the recursive de nition of atl
ir formulae is:
ϕ ::= p | ¬ϕ | ϕ ∧ ϕ | hhAiiir gϕ | hhAiiir ϕ | hhAiiir ϕ U ϕ
Again, we de ne hhAiiir ♦ϕ ≡ hhAiiir > U ϕ.
Models of atlir , imperfect information concurrent game structures (i cgs
), can be presented
as concurrent game structures augmented with a family of epistemic indistinguishability relations
∼a ⊆ St × St, one per agent a ∈ Agt. The relations describe agents' uncertainty: q ∼a q 0 means
that, while the system is in state q , agent a considers it possible that it is in q 0 now. It is required
that agents have the same choices in indistinguishable states. To recapitulate, i cgs
can be de ned
as tuples
M = hAgt, St, Π, π, Act, d, o, ∼1 , ..., ∼k i,
where:
• Agt = {1, ..., k} is a nite nonempty set of all agents,
• St is a nonempty set of states,
• Π is a set of atomic propositions,
• π : Π → P(St) is a valuation of propositions,
• Act is a nite nonempty set of (atomic) actions;
• function d : Agt × St → P(Act) de nes actions available to an agent in a state; d(a, q) 6= ∅
for all a ∈ Agt, q ∈ St,
• o is a (deterministic) transition function that assigns outcome states to states and tuples of
actions; that is, o(q, α1 , . . . , αk ) ∈ St for every q ∈ St and hα1 , . . . , αk i ∈ d(1, q) × · · · × d(k, q);
• ∼1 , ..., ∼k ⊆ St × St are epistemic relations, one per agent. Every ∼a is assumed to be an
equivalence. We require that q ∼a q 0 implies d(a, q) = d(a, q 0 ).
Again, a (memoryless) strategy of agent a is a conditional plan that speci es what a is going to
do in every possible state. An executable plan must prescribe the same choices for indistinguishable
states. Therefore atlir restricts the strategies that can be used by agents to the set of so called
uniform strategies. A uniform strategy of agent a is de ned as a function sa : St → Act, such that:
(1) sa (q) ∈ d(a, q), and (2) if q ∼a q 0 then sa (q) = sa (q 0 ). A collective strategy for a group of agents
A = {a1 , ..., ar } is a tuple of strategies SA = hsa1 , ..., sar i, one per agent from A. A collective
strategy is uniform if it contains only uniform individual strategies. Again, function out(q, SA )
returns the set of all paths that may result from agents A executing strategy SA from state q
onward:3
3 The notation S (a) stands for the strategy s of agent a in the tuple S = hs , ..., s i.
A a A a1 ar
q0
b
qAK a qAQ b qKQ a qKA b qQA a qQK
keep,nop keep,chg keep,nop
exch,chg keep,chg exch,chg keep,nop exch,chg
exch,nop keep,nop exch,nop exch,nop
keep,chg exch,nop exch,chg keep,chg
keep,nop keep,nop
keep,chg
exch,chg w q keep,chg
q
l
exch,chg
exch,nop
exch,nop win
Figure 1: Gambling Robots game
out(q, SA ) = {λ = q0 q1 q2 ... | q0 = q and for every i = 1, 2, ... there exists a tuple of agents' decisions
hα1i−1 , ..., αki−1 i such that αai−1 = SA (a)(qi−1 ) for each a ∈ A, αai−1 ∈ d(a, qi−1 ) for each a ∈
/ A,
and o(qi−1 , α1i−1 , ..., αki−1 ) = qi }.
The semantics of atl
ir formulae is de ned as follows. The rst three lines are obvious, similar
to the de nition of truth in Kripke models. While the rst states that an atomic proposition is
true in a model and a state i the valuation makes it true in this state, the next two lines de ne
the usual meaning of ¬ϕ and ϕ ∧ ψ . Lines 46 de ne the meaning of cooperation modalities.
M, q |= p i q ∈ π(p) (for p ∈ Π);
M, q |= ¬ϕ i M, q 6|= ϕ;
M, q |= ϕ ∧ ψ i M, q |= ϕ and M, q |= ψ ;
M, q |= hhAiiir gϕ i there exists a uniform strategy SA such that, for every a ∈ A, q 0 ∈ St such
that q ∼a q 0 , and λ ∈ out(SA , q 0 ), we have M, λ[1] |= ϕ;
M, q |= hhAiiir ϕ i there exists a uniform strategy SA such that, for every a ∈ A, q 0 ∈ St such
that q ∼a q 0 , and λ ∈ out(SA , q 0 ), we have M, λ[i] |= ϕ for every i ≥ 0;
M, q |= hhAiiir ϕ U ψ i there exist a uniform strategy SA such that, for every a ∈ A, q 0 ∈ St such
that q ∼a q 0 , and λ ∈ out(SA , q 0 ), there is i ≥ 0 for which M, λ[i] |= ψ , and M, λ[j] |= ϕ for
every 0 ≤ j < i.
That is, hhAiiir ϕ if coalition A has a uniform strategy, such that for every path that can possibly
result from execution of the strategy according to at least one agent from A, ϕ is the case. This is
a strong requirement, because it su ces that at least one of the agents in A considers some states
q, q 0 equivalent: then, all relevant paths starting from both q and q 0 must be considered.
Note that the universal path quanti er A (for every path) from ctl
can be expressed in ir atl
as hh∅iiir .
Example 1 (Gambling robots) Two robots (a and b) play a simple card game. The deck consists
of Ace, King and Queen (A, K, Q). Normally, it is assumed that A is the best card, K the second
best, and Q the worst. Therefore A beats K and Q, K beats Q, and Q beats no card. At the
beginning of the game, the environment agent deals a random card to both robots (face down), so
that each player can see his own hand, but he does not know the card of the other player. Then
robot a can exchange his card for the one remaining in the deck (action exch), or he can keep the
current one (keep). At the same time, robot b can change the priorities of the cards, so that Q
becomes better than A (action chg ) or he can do nothing (nop), i.e. leave the priorities unchanged.
If a has a better card than b after that, then a win is scored, otherwise the game ends in a losing
state. An i cgs M1 for the game is shown in Figure 1.
It is easy to see that M1 , q0 |= ¬hhaiiir ♦win, because, for every a's (uniform) strategy, if it guar-
antees a win in e.g. state qAK then it fails in qAQ (and similarly for other pairs of indistinguishable
states). Let us also observe that M1 , q0 |= ¬hha, biiir ♦win (in order to win, a must exchange his
card in state qQK , so he must exchange his card in qQA too (by uniformity), and playing exch in
qQA leads to the losing state). On the other hand, M1 , qAQ |= hha, biiir gwin (a winning strategy:
sa (qAK ) = sa (qAQ ) = sa (qKQ ) = keep, sb (qAQ ) = sb (qKQ ) = sb (qAK ) = nop; qAK , qAQ , qKQ are
the states that must be considered by a and b in qAQ ). Still, M1 , qAK |= ¬hha, biiir gwin.
Schobbens [18] proved that atl
ir model checking is NP-hard and ∆2 -easy. He also conjectured
P
that the problem is ∆2 -complete. We prove that it is indeed the case in Section 3.
P
3 Model Checking ATLir
Schobbens [18] proved that atlir model checking is intractable: more precisely, it is NP-hard and
∆P 2 -easy when the size of the model is de ned in terms of the number of transitions. He also
conjectured that the problem is ∆P 2 -complete. In this section, we close the gap and prove that it
is ∆P -hard, and hence indeed ∆ 2 -complete. The proof proceeds by a reduction of the SNSAT
P
atl
2
problem to ir model checking, presented in Section 3.2.
A problem is in ∆P 2 = P NP
if it can be solved in deterministic polynomial time with subcalls to
an NP-oracle (we refer the reader to [17, 3] for more detailed information about complexity classes
and their complete problems). Class ∆P 2 belongs to the rst level of the polynomial hierarchy
(although the index suggests it belongs to the second level). The class is supposed to be just above
NP (unless the polynomial hierarchy collapses):
NP ∪ co-NP ⊆ ∆P P P
2 ⊆ Σ2 ∩ Π2 .
where ΣP2 = NP
NP
, and ΠP
2 = co-NP
NP
.
We have already investigated the complexity of atl
ir model checking in [11], concluding that
the problem is NP-complete. Unfortunately, our claim was incorrect: we set it right in this paper.
3.1 Existing Results
Model checking atl ir has been proved to be NP-hard and ∆2 -easy in the number of transitions
P
and the length of the formula [18]. The membership in ∆2 was demonstrated through the following
P
observation. If the formula to be model checked is of the form hhAiiir ϕ (ϕ being gψ , ψ or ψ1 U ψ2 ),
where ϕ contains no more cooperation modalities, then it is su cient to guess a strategy for A,
trim the model by removing all transitions that will never be executed (according to this strategy),
and model check ctl formula Aϕ in the resulting model. Thus, model checking an arbitrary ir atl
formula can be done by checking the subformulae iteratively, which requires a polynomial number
of calls to an NP algorithm.4
The NP-hardness follows from a reduction of the well known SAT problem. Here, we present a
reduction which is somewhat dierent from the one in [18]. We will adapt it in Section 3.2 to prove
∆P 2 -hardness. In SAT, we are given a CNF formula ϕ ≡ C1 ∧ . . . ∧ Cn involving k propositional
s s
variables from set X = {x1 , ..., xk }. Each clause Ci can be written as Ci ≡ x1i,1 ∨ . . . ∨ xki,k , where
−
si,j ∈ {+, −, 0}; x+ j denotes a positive occurrence of xj in Ci , xj denotes an occurrence of ¬xj in
Ci , and xj indicates that xj does not occur in Ci . The problem asks if ∃X.ϕ, that is, if there is a
0
valuation of x1 , ..., xk such that ϕ holds.
We construct the corresponding i cgsMϕ as follows. There are two players: veri er v and refuter
r. The refuter decides at the beginning of the game which clause Ci will have to be satis ed: it
is done by proceeding from the initial state q0 to a clause state qi . At qi , veri er decides (by
s
proceeding to a proposition state qi,j ) which of the literals xj i,j from Ci will be attempted.
Finally, at qi,j , veri er attempts to prove Ci by declaring the underlying propositional variable xj
true (action >) or false (action ⊥). If she succeeds (i.e., if she executes > for x+ j , or executes ⊥
for x−j ), then the system proceeds to the winning state q > . Otherwise, the system stays in qi,j .
Additionally, proposition states referring to the same variable are indistinguishable for veri er, so
4 The algorithm from [11] can be also used to demonstrate the upper bounds for the complexity of this problem.
x1
v:1 q1,1 ^
v:
q1 Øx3
r:1 v:3 q1,3 v:^
q0 q^
Øx1 yes
v:^
q2,1 ^
r:2 v:1 x v:
q2 v:2 2 q 2,2
v:3 ^
q2,3 v:
x3
Figure 2: An i cgs for checking satis ability of ϕ ≡ (x1 ∨ ¬x3 ) ∧ (¬x1 ∨ x2 ∨ x3 )
that she has to declare the same value of xj in all of them within a uniform strategy. A sole ir atl
proposition yes holds only in the winning state q> . Obviously, states corresponding to literals x0j
can be omitted from the model.
Speaking more formally, Mϕ = hAgt, St, Π, π, Act, d, o, ∼1 , ..., ∼k i, where:
• Agt = {v, r},
• St = {q0 } ∪ Stcl ∪ Stprop ∪ {q> },
where Stcl = {q1 , . . . , qn }, and Stprop = {q1,1 , . . . , q1,k , . . . , qn,1 , . . . , qn,k };
• Π = {yes}, π(yes) = {q> },
• Act = {1, ..., max(k, n), >, ⊥},
• d(v, q0 ) = d(v, q> ) = {1}, d(v, qi ) = {1, ..., k}, d(v, qi,j ) = {>, ⊥};
d(r, q) = {1, ..., n} for q = q0 , and d(r, q) = {1} otherwise;
• o(q0 , 1, i) = qi , o(qi , j, 1) = qi,j ,
o(qi,j , >, 1) = q> if si,j = +, and qi,j otherwise,
o(qi,j , ⊥, 1) = q> if si,j = −, and qi,j otherwise;
• q0 ∼v q i q = q0 , qi ∼v q i q = qi , qi,j ∼v q i q = qi0 ,j .
As an example, model Mϕ for ϕ ≡ (x1 ∨ ¬x3 ) ∧ (¬x1 ∨ x2 ∨ x3 ) is presented in Figure 2.
Theorem 2 ϕ is satis able i Mϕ , q0 |= hhviiir ♦yes.
Proof.
(⇒) Firstly, if there is a valuation that makes ϕ true, then for every clause Ci one can choose
a literal out of Ci that is made true by the valuation. The choice, together with the valuation,
corresponds to a uniform strategy for v such that, for all possible executions, q> is achieved at the
end.
(⇐) Conversely, if Mϕ , q0 |= hhviiir ♦yes, then there is a strategy sv such that q> is achieved for
all paths from out(q0 , sv ). But then the valuation, which assigns propositions x1 , ..., xk with the
same values as sv , satis es ϕ.
Both the number of states and transitions in Mϕ are linear in the length of ϕ, and the construc-
tion of M requires linear time too. Thus, the model checking problem for atl
ir is NP-hard. Note
that it is NP-hard even for formulae with a single cooperation modality, and turn-based models
with at most two agents.5
We already investigated the complexity of atl
ir model checking in [11], concluding that the
problem was NP-complete. Unfortunately, our claim was incorrect: the error occurred in the way
we handled negation in our model checking algorithm (cf. [16]). Still, as observed by Laroussinie,
Markey and Oreiby in [16], our algorithm is correct for positive ir i.e., ir withoutatl atl
negation. Thus, the following holds.
Proposition 3 Model checking of positive atl
ir is NP-complete with respect to the number of
transitions in the model and the length of the formula.
The ∆P
2 -hardness for the full atlir is proved in Section 3.2.
3.2 Model Checking ATLir Is Indeed ∆P
2 -complete
Let us rst recall (after [16]) the de nition of SNSAT, a typical ∆P
2 -hard problem.
De nition 1 (SNSAT)
Input: p sets of propositional variables Xr = {x1,r , ..., xk,r }, p propositional variables zr , and p
Boolean formulae ϕr in CNF, with each ϕr involving only variables in Xr ∪ {z1 , ..., zr−1 }, with the
following requirement:
zr ≡ there exists an assignment of variables in Xr such that ϕr is true.
We will also write, by abuse of notation, zr ≡ ∃Xr ϕr (z1 , ..., zr−1 , Xr ).
Output: The truth-value of zp (i.e., > or ⊥).
Let n be the maximal number of clauses in any ϕ1 , ..., ϕp from the given input. Now, each ϕr
can be written as:
sri,1 sri,k sri,k+1 sri,k+r−1
ϕr ≡ C1r ∧ . . . ∧ Cnr , r
and Ci ≡ x1,r ∨ . . . ∨ xk,r ∨ z1 ∨ . . . zr−1 .
Again, sri,j ∈ {+, −, 0}; x+ denotes a positive occurrence of x, x− denotes an occurrence of ¬x, and
x0 indicates that x does not occur in the clause. Similarly, sri,k+j de nes the sign of zj in clause
Cir . Given such an instance of SNSAT, we construct a sequence of concurrent game structures Mr
for r = 1, ..., p in a similar way to the construction in Section 3.1. That is, clauses and variables
xi,r are handled in exactly the same way as before. Moreover, if zi occurs as a positive literal in
ϕr , we embed Mi in Mr , and add a transition to the initial state q0i of Mi . If ¬zi occurs in ϕr , we
do almost the same: the only dierence is that we split the transition into two steps, with a state
negir (labeled with an atl
ir proposition neg) added in between.
More formally, Mr = hAgt, Str , Π, π r , Actr , dr , or , ∼r1 , ..., ∼rk i, where:
• Agt = {v, r},
• Str = {q0r , q1r , . . . , qnr , q1,1
r r
, . . . , qn,k , neg1r , . . . , negr−1
r
, q> } ∪ Str−1 ,
• Π = {yes, neg}, π r (yes) = {q> }, π r (neg) = {negij | i, j = 1, ..., r},
• Actr = {1, ..., max(k + r − 1, n), >, ⊥},
• dr (v, q0r ) = dr (v, negir ) = dr (v, q> ) = {1}, dr (v, qir ) = {1, ..., k + r − 1},
d (v, qi,j ) = {>, ⊥},
r r
dr (r, q) = {1, ..., n} for q = q0r and {1} for the other q ∈ Str .
For q ∈ Str−1 , we simply include the function from Mr−1 : dr (a, q) = dr−1 (a, q);
• or (q0r , 1, i) = qir , or (qir , j, 1) = qi,j
r
for j ≤ k ,
o (qi , k + j, 1) = qj if si,k+j = +, and or (qir , k + j, 1) = negjr if sri,k+j = −,
r r r
or (negjr , 1, 1) = qj ,
or (qi,j
r
, >, 1) = q> if sri,j = +, and qi,j r
otherwise,
or (qi,j
r
, ⊥, 1) = q> if sri,j = −, and qi,j r
otherwise.
For q ∈ St , we include the transitions from Mr−1 : or (q, α) = or−1 (q, α);
r−1
5 In fact, it is NP-hard even for models with a single agent, although the construction must be a little dierent
to demonstrate this.
M3 q0
r:1 r:2
q1 q2
v:1 v:2 v:1 v:2
x3 Øx3
Øz2 neg2 q1,1 neg1 Øz1 q2,1
neg neg
v:
^ v:^
M2 M1 x1
q1,1
v:1 ^
v:
q1 x2
q1 z1
r:1 v:2 q1,2 v:
^
r:1
q0 q^
Øx1
q0 r:2 v:1 v:^
yes
neg q2 q2,1
r:2
q2 neg1Øz
1
Figure 3: An i cgs for the reduction of SNSAT
• q0r ∼v q i q = q0r , qir ∼v q i q = qir , r
qi,j ∼v q i q = qir0 ,j .
For q, q 0 ∈ Str−1 , we include the tuples from Mr−1 : q ∼rv q 0 i q ∼vr−1 q 0 .
As an example, model M3 for ϕ3 ≡ (x3 ∨ ¬z2 ) ∧ (¬x3 ∨ ¬z1 ), ϕ2 ≡ z1 ∧ ¬z1 , ϕ1 ≡ (x1 ∨ x2 ) ∧ ¬x1 ,
is presented in Figure 3.
Theorem 4 Let
Φ1 ≡ hhviiir (¬neg) U yes,
Φi ≡ hhviiir (¬neg) U (yes ∨ (neg ∧ A g¬Φi−1 )).
r
Now, for all r : zr is true i Mr , q0 |= Φr .
Before we prove the theorem, we state an important lemma. Lemma 5 says that overlong
formulae Φi do not introduce new properties of model Mr . More precisely, a formula Φi that
includes more nestings than model Mr can be as well reduced to Φi−1 when model checked in
Mr , q0r .
Lemma 5 For i ≥ r: Mr , q0r |= Φi i Mr , q0r |= Φi+1 .
Proof (induction on r ).
1. For r = 1: M1 , q01 |= Φi i M1 , q01 |= hhviiir ♦yes i M1 , q01 |= Φi+1 , because M1 does not
include states that satisfy neg.
2. For r > 1: Mr , q0r |= Φi+1 ≡ hhviiir (¬neg) U (yes∨(neg∧A g¬Φi )) i ∃sv ∀λ ∈ out(q0r , sv )∃u
∀w ≤ u. (Mr , λ[u] |= yes or Mr , λ[u] |= neg ∧ A g¬Φi ) and (Mr , λ[w] |= ¬neg) . [*]
However, each state satisfying neg has exactly one outgoing transition, so Mr , λ[u] |= neg ∧
A g¬Φi is equivalent to Mr , λ[u] |= neg and Mr , λ[u + 1] |= ¬Φi . Thus, [*] i ∃sv ∀λ ∈
out(q0r , sv )∃u∀w ≤ u. (Mr , λ[u] |= yes or Mr , λ[u] |= neg and Mr , λ[u + 1] |= ¬Φi ) and
(Mr , λ[w] |= ¬neg) [**].
Note that, by the construction of Mr , λ[u + 1] must refer to the initial state q0j of some
submodel Mj , j < r ≤ i. Thus, Mr , λ[u + 1] |= ¬Φi i Mj , q0j |= ¬Φi i (by induction)
Mj , q0j |= ¬Φi−1 i Mj , λ[u + 1] |= ¬Φi−1 .
So, [**] i ∃sv ∀λ ∈ out(q0r , sv )∃u∀w
≤ u. (Mr , λ[u] |= yes or Mr , λ[u] |= neg and Mr , λ[u+
1] |= ¬Φi−1 ) and (Mr , λ[w] |= ¬neg) i Mr , q0r |= hhviiir (¬neg) U (yes∨(neg∧A g¬Φi−1 )) ≡
Φi .
Proof of Theorem 4 (induction on r ).
1. For r = 1: we use the proof of Theorem 2.
2. For r > 1:
For the implication from left to right (⇒): let zr be true: then, there is a valuation
of Xr such that ϕr holds. We construct sv as in the proof of Theorem 2. In case that some
xsi has been chosen in clause Cir , we are done. In case that some zj− has been chosen in
clause Cir (note: j must be smaller than i), we have (by induction) that Mj , q0j |= ¬Φj . By
Lemma 5, also Mj , q0j |= ¬Φr , and hence Mr , q0j |= ¬Φr . So we can make the same choice
(i.e., zj− ) in sv , and this will lead to state negjr , in which it holds that neg ∧ A g¬Φr .
In case that some zj+ has been chosen in clause Cir , we have (by induction) that Mj , q0j |= Φj ,
and hence, by Lemma 5, Mj , q0j |= Φr . That is, there is a strategy s0v in Mj such that
(¬neg) U (yes ∨ (neg ∧ A g¬Φr−1 )) holds for all paths from out(q0j , s0v ). As the states in Mj
have no epistemic links to states outside of it, we can merge s0v into sv .
For the other direction (⇐): let Mr , q0r |= Φr ≡ hhviiir (¬neg) U (yes ∨ (neg ∧ A g¬Φr−1 )).
We take the strategy sv that enforces (¬neg) U (yes ∨ (neg ∧ A g¬Φr−1 )). We rst consider
the clause Cir for which a propositional state is chosen by sv . The strategy de nes a uniform
valuation for Xr that satis es these clauses. For the other clauses, we have two possibilities:
• sv chooses q0j in the state corresponding to Cir . Neither yes nor neg have been encountered
on this path yet, so we can take sv to demonstrate that Mr , q0j |= Φr , and hence Mj , q0j |=
Φr . By Lemma 5, also Mj , q0j |= Φj . By induction, zj must be true, and hence clause
Cir is satis ed.
• sv chooses negjr in the state corresponding to Cir . Then, it must be that Mr , negjr |=
A g¬Φr−1 , and hence Mj , q0j |= ¬Φr−1 . By Lemma 5, also Mj , q0j |= ¬Φj . By induction,
zj must be false, and hence clause Cir (containing ¬zj ) is also satis ed.
Thus, in order to determine the value of zp , it is su cient to model check Φp in Mp , q0p . Note
that model Mp consists of O(|ϕ|p) states and O(|ϕ|p) transitions, where |ϕ| is the maximal length
of formulae ϕ1 , ..., ϕp . Moreover, the length of formula Φp is linear in p, and the construction of
Mp and Φp can be also done in time O(|ϕ|p) and O(p), respectively. In consequence, we obtain a
polynomial reduction of SNSAT to atl ir model checking.
Theorem 6 Model checking atlir is ∆P2 -complete with respect to the number of transitions in the
P
model, and the length of the formula. The problem is ∆2 -complete even for turn-based models with
at most two agents.
4 Conclusions
In this paper we proved that model checking of atl ir formulae is ∆2 -hard, and therefore ∆2 -
P P
complete. Thus, we closed an existing gap (between NP-hardness and ∆2 -easiness) in the work
P
of Schobbens [18], and at the same time corrected our own claim from [11].
While it is possible that NP and ∆P 2 are identical, many believe that ∆2 is a strict superset
P
of NP. Still, NP and ∆2 are quite close, both belonging to the rst level of the polynomial
P
hierarchy. Therefore our result might seem a minor one although, technically, it was not that
trivial to prove it. On the other hand, its importance goes well beyond model checking of atlir . In
fact, Theorem 6 yields immediate corollaries with ∆P atol
2 -completeness of other logics like [12],
Feasibleatel csl
[15], [13] etc., and ∆P etsl
2 -hardness of [22].
We would like to thank Nils Bulling for careful reading of our proofs.
References
[1] R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time Temporal Logic. In Proceedings
of the 38th Annual Symposium on Foundations of Computer Science (FOCS), pages 100109.
IEEE Computer Society Press, 1997.
[2] R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time Temporal Logic. Journal of
the ACM, 49:672713, 2002.
[3] J.L. Balcázar, J. Diaz, and J. Gabarró. Structural Complexity I. Springer-Verlag, 1988.
[4] E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using
branching time temporal logic. In Proceedings of Logics of Programs Workshop, volume 131 of
Lecture Notes in Computer Science, pages 5271, 1981.
[5] E. A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical
Computer Science, volume B, pages 9951072. Elsevier Science Publishers, 1990.
[6] V. Goranko. Coalition games and alternating temporal logics. In J. van Benthem, editor,
Proceedings of TARK VIII, pages 259272. Morgan Kaufmann, 2001.
[7] V. Goranko and W. Jamroga. Comparing semantics of logics for multi-agent systems. Synthese,
139(2):241280, 2004.
[8] A. Herzig and N. Troquard. Knowing how to play: Uniform choices in logics of agency. In
Proceedings of AAMAS'06, 2006.
[9] W. Jamroga. Some remarks on alternating temporal epistemic logic. In B. Dunin-Keplicz and
R. Verbrugge, editors, Proceedings of Formal Approaches to Multi-Agent Systems (FAMAS
2003), pages 133140, 2003.
[10] W. Jamroga and J. Dix. Do agents make model checking explode (computationally)? In
M. Pechoucek, P. Petta, and L.Z. Varga, editors, Proceedings of CEEMAS 2005, volume 3690
of Lecture Notes in Computer Science, pages 398407. Springer Verlag, 2005.
[11] W. Jamroga and J. Dix. Model checking strategic abilities of agents under incomplete infor-
mation. In M. Coppo, E. Lodi, and G.M. Pinna, editors, Proceedings of ICTCS 2005, volume
3701 of Lecture Notes in Computer Science, pages 295308. Springer Verlag, 2005.
[12] W. Jamroga and W. van der Hoek. Agents that know how to play. Fundamenta Informaticae,
63(23):185219, 2004.
[13] W. Jamroga and Thomas Ågotnes. Constructive knowledge: What agents can achieve under
incomplete information. Technical Report IfI-05-10, Clausthal University of Technology, 2005.
[14] Wojciech Jamroga and Thomas Ågotnes. What agents can achieve under incomplete informa-
tion. In Proceedings of AAMAS'06, 2006.
[15] G. Jonker. Feasible strategies in Alternating-time Temporal Epistemic Logic. Master thesis,
University of Utrecht, 2003.
[16] F. Laroussinie, N. Markey, and G. Oreiby. Expressiveness and complexity of ATL. Technical
Report LSV-06-03, CNRS & ENS Cachan, France, 2006.
[17] C.H. Papadimitriou. Computational Complexity. Addison Wesley : Reading, 1994.
[18] P. Y. Schobbens. Alternating-time logic with imperfect recall. Electronic Notes in Theoretical
Computer Science, 85(2), 2004.
[19] W. van der Hoek, A. Lomuscio, and M. Wooldridge. On the complexity of practical ATL
model checking. In P. Stone and G. Weiss, editors, Proceedings of AAMAS'06, pages 201208,
2006.
[20] W. van der Hoek and M. Wooldridge. Tractable multiagent planning for epistemic goals.
In C. Castelfranchi and W.L. Johnson, editors, Proceedings of the First International Joint
Conference on Autonomous Agents and Multi-Agent Systems (AAMAS-02), pages 11671174.
ACM Press, New York, 2002.
[21] W. van der Hoek and M. Wooldridge. Cooperation, knowledge and time: Alternating-time
Temporal Epistemic Logic and its applications. Studia Logica, 75(1):125157, 2003.
[22] S. van Otterloo and G. Jonker. On Epistemic Temporal Strategic Logic. Electronic Notes in
Theoretical Computer Science, XX:3545, 2004. Proceedings of LCMAS'04.