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 Δ2P-complete, thus conrming the initial intuition of Schobbens [18]. We prove Δ2P-hardness through a reduction of the SNSAT problem, while the membership in Δ2P stems from the algorithm presented in [18].
ATL: Ability in Perfect Information Games
Atl is a generalization of the branching time temporal logic ctl [
A number of semantics have been dened for atl, most of them equivalent [
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
inspection, 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 [
Proposition 1 ([
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 dene 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],[
Atlir 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 Atlir 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 denition of atlir formulae is:
ϕ ::= p | ¬ϕ | ϕ ∧ ϕ | hhAiiir gϕ | hhAiiir ϕ | hhAiiirϕ U ϕ
Models of atlir, imperfect information concurrent game structures (icgs), 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 q0 means that, while the system is in state q, agent a considers it possible that it is in q0 now. It is required that agents have the same choices in indistinguishable states. To recapitulate, icgs can be dened as tuples
M = hAgt, St, Π, π, Act, d, o, ∼1, ..., ∼ki, 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) denes actions available to an agent in a state; for all a ∈ Agt, q ∈ St, d(a, q) 6= ∅ • 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, . . . , αki ∈ 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 q0 implies d(a, q) = d(a, q0).
Again, a (memoryless) strategy of agent a is a conditional plan that species 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 dened as a function sa : St → Act, such that: (1) sa(q) ∈ d(a, q), and (2) if q ∼a q0 then sa(q) = sa(q0). 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 3The notation SA(a) stands for the strategy sa of agent a in the tuple SA = hsa1 , ..., sar i.
KA QA keep,chg keep,nop keep,nop exch,chg exch,nopexch,nop exch,chg keep,chg
keep,nop ql a q
QK exch,chg exch,nop out(q, SA) = {λ = q0q1q2... | q0 = q and for every i = 1, 2, ... there exists a tuple of agents’ decisions hα1i−1, ..., αki−1i 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 atlir formulae is dened as follows. The rst three lines are obvious, similar to the denition 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 dene the usual meaning of ¬ϕ and ϕ ∧ ψ. Lines 46 dene the meaning of cooperation modalities. M, q |= p i q ∈ π(p) M, q |= ¬ϕ i
M, q 6|= ϕ;
(for p ∈ Π); 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, q0 ∈ St such
that q ∼a q0, and λ ∈ out(SA, q0), we have M, λ[
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 suces that at least one of the agents in A considers some states q, q0 equivalent: then, all relevant paths starting from both q and q0 must be considered.
Note that the universal path quantier A (for every path) from ctl can be expressed in atlir 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 icgs 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 guarantees 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 [
Schobbens [
A problem is in Δ2P = PNP if it can be solved in deterministic polynomial time with subcalls to
an NP-oracle (we refer the reader to [
NP ∪ co-NP ⊆ Δ2P ⊆ Σ2P ∩ Π2P. where Σ2P = NPNP, and Π2P = co-NPNP.
We have already investigated the complexity of atlir model checking in [
Existing Results
Model checking atlir has been proved to be NP-hard and Δ2P-easy in the number of transitions
and the length of the formula [
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 [
We construct the corresponding icgs Mϕ as follows. There are two players: verier v and refuter
r. The refuter decides at the beginning of the game which clause Ci will have to be satised: it
is done by proceeding from the initial state q0 to a clause state qi. At qi, verier decides (by
proceeding to a proposition state qi,j ) which of the literals xjsi,j from Ci will be attempted.
Finally, at qi,j , verier 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 xj+, or executes ⊥
for xj−), 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 verier, so
4The algorithm from [
Speaking more formally, Mϕ = hAgt, St, Π, π, Act, d, o, ∼1, ..., ∼ki, 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 satisable 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, satises ϕ.
Both the number of states and transitions in Mϕ are linear in the length of ϕ, and the construction of M requires linear time too. Thus, the model checking problem for atlir 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 atlir model checking in [
Proposition 3 Model checking of positive atlir is NP-complete with respect to the number of transitions in the model and the length of the formula.
3.2
Let us rst recall (after [
Denition 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: ϕr ≡ C1r ∧ . . . ∧ Cnr , and Cir ≡ xs1i,r,1 ∨ . . . ∨ xski,,rk ∨ z1sir,k+1 ∨ . . . zrs−ir,k1+r−1 .
r r Again, sir,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, sir,k+j denes the sign of zj in clause Cr. Given such an instance of SNSAT, we construct a sequence of concurrent game structures Mr i 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 atlir proposition neg) added in between.
More formally, Mr = hAgt, Str, Π, πr, Actr, dr, or, ∼r1, ..., ∼rki, where: • Agt = {v, r}, • Str = {q0r, q1r, . . . , qnr, q1r,1, . . . , qnr,k, neg1r, . . . , negrr−1, q>} ∪ Str−1, • Π = {yes, neg},
πr(yes) = {q>}, • Actr = {1, ..., max(k + r − 1, n), >, ⊥},
πr(neg) = {negij | i, j = 1, ..., r}, • dr(v, q0r) = dr(v, negir) = dr(v, q>) = {1}, dr(v, qir) = {1, ..., k + r − 1}, dr(v, qir,j ) = {>, ⊥}, 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) = qir,j for j ≤ k, or(qir, k + j, 1) = qj if sir,k+j = +, and or(qir, k + j, 1) = negjr if sir,k+j = −, or(negjr, 1, 1) = qj , oorr((qqiirr,,jj ,, ⊥>,, 11)) == qq>> iiff ssiirr,,jj == −+,, aanndd qqiirr,,jj ootthheerrwwiissee,.
For q ∈ Str−1, we include the transitions from Mr−1: or(q, α) = or−1(q, α); 5In fact, it is NP-hard even for models with a single agent, although the construction must be a little dierent to demonstrate this. neg x3 q r:1 neg1 neg
z1 M
2 q 0 r:1 r:2 q
1 q 2 neg neg1 z 1 v:2
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)).
Now, for all r: zr is true i Mr, q0r |= Φr.
Mr, q0r.
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 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 include states that satisfy neg.
M1, q01 |= hhviiir♦yes i M1, q01 |= Φi+1, because M1 does not 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 xis 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.
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 denes a uniform valuation for Xr that satises these clauses. For the other clauses, we have two possibilities: • sv chooses q0j in the state corresponding to Cr. Neither yes nor neg have been encountered i 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 satised. • sv chooses negjr in the state corresponding to Cr. Then, it must be that Mr, negjr |= i 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 satised.
Thus, in order to determine the value of zp, it is sucient 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 atlir model checking.
Theorem 6 Model checking atlir is Δ2P-complete with respect to the number of transitions in the model, and the length of the formula. The problem is Δ2P-complete even for turn-based models with at most two agents.
In this paper we proved that model checking of atlir formulae is Δ2P-hard, and therefore
Δ2Pcomplete. Thus, we closed an existing gap (between NP-hardness and Δ2P-easiness) in the work
of Schobbens [
While it is possible that NP and Δ2P are identical, many believe that Δ2P is a strict superset
of NP. Still, NP and Δ2P are quite close, both belonging to the rst level of the polynomial
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 Δ2P-completeness of other logics like atol [
We would like to thank Nils Bulling for careful reading of our proofs.