Some Things are Easier for the Dumb and the Bright Ones (Beware the Average!)

1 Introduction

Many relevant properties of multi-agent systems (MAS) refer to strategic abilities of agents and their groups. Such properties can be neatly specified in alternating-time temporal logic (ATL) [Alur et al., 2002]. In its basic version, the logic allows to specify strategic properties of agents and their coalitions under the assumption of perfect information about the current state of affairs. As the assumption is rather unrealistic, there is a growing number of works that study the syntactic and semantic variants of ATL for agents with imperfect information, cf. [ ˚Agotnes et al., 2015] for an overview.

Unfortunately, verification of strategic properties of agents with imperfect information is difficult. More precisely, model checking of ATL variants with imperfect information is ∆P2 - to PSPACE-complete for agents playing memoryless (a.k.a. positional) strategies [Bulling et al., 2010; Jamroga and Dix, 2006; Schobbens, 2004] and EXPTIMEcomplete to undecidable for agents with perfect recall of the past [Dima and Tiplea, 2011; Guelev et al., 2011]. This concurs with the results for solving imperfect information games and synthesis of winning strategies, which are also known to be hard [Doyen and Raskin, 2011; Chatterjee et al., 2007; Peterson and Reif, 1979]. Note, however, that theoretical complexity results refer to the worst case complexity. The problem might as well be easier when restricted to a particular subclass of inputs. Indeed, many hard problems have relatively small "hardness cores," and are fairly easy elsewhere. In the context of model checking for strategies, such results are especially known for strategies with perfect recall [Schewe and Finkbeiner, 2007; Berwanger and Kaiser, 2010; Belardinelli et al., 2017; Berwanger et al., 2018; Maubert and Murano, 2018].

In this paper, we study some natural restrictions on models, that might lead to cheaper verification. More specifically, we look at models with "extreme" epistemic structure, arising when the agents have almost nil, or, symmetrically, almost perfect observability. A sensor observing only one variable, with a fixed number of possible values, provides a natural example of the former type. For the latter class, consider a central controller monitoring a team of robots, with only a fixed number of units being unavailable at a time. It turns out that, when we consistently pair those restrictions with the assumptions about agents' memory (i.e., assume almost perfect observability and perfect recall, or almost nil observability and no recall), model checking can become easier than in general. This applies especially to the verification of abilities of singleton coalitions. We also show that no gain is possible for the other combinations. To prove the latter kind of results, we develop general reduction techniques which may be relevant also for other formal problems in AI.

2 Model Checking Strategic Abilities

2.1 ATL: What Agents Can Achieve

Alternating-time temporal logic ATL [Alur et al., 2002] generalizes branching time logic CTL by replacing path quantifiers with cooperation modalities 〈〈A〉〉. Informally, 〈〈A〉〉γ expresses that the group of agents A has a collective strategy to enforce temporal property γ. ATL formulae include temporal operators: "X" ("in the next state"), "G" ("always from now on") and U ("until"). The additional operator "F" ("now or sometime in the future") is defined as Fγ ≡ ⊤Uγ.

The language of ATL is given by the grammar below, where A is a set of agents, and p is an atomic proposition:

2.2 Models of Multi-Agent Interaction

The semantics of ATL is defined over a variant of transition systems where transitions are labeled with combinations of actions, one per agent. Formally, a concurrent game structure (CGS) [Alur et al., 2002] is a tuple M = 〈Agt, St,Π, π,Act, d, o〉 which includes a nonempty finite set of all agents Agt = {1, . . . , k}, a nonempty set of states St, a set of atomic propositions Π and their valuation π : Π → 2St , and a nonempty finite set of (atomic) actions Act. Function d : Agt × St → 2Act \ ∅ defines the sets of actions available to agents at each state. We will often write di(q) instead of d(i, q), and denote the set of collective choices of group A at state q by dA(q) = ∏i∈A di(q). Finally, o is a transition function that assigns the outcome state q′ = o(q, α1, . . . , αk) to state q and a tuple of actions αi ∈ dAgt(q).

Concurrent epistemic game models (CEGM) [Schobbens, 2004], are CGS's augmented with a family of equivalence relations ∼a⊆ St ×St, one per agent a ∈ Agt. The relations describe agents' uncertainty: q ∼a q′ means that agent a cannot distinguish between states q and q′ . It is also required that agents have the same choices in indistinguishable states: if q ∼a q′ then da(q) = da(q′ ). The abstraction classes of ∼a are sometimes called information sets. We use #is to denote the maximum number of information sets per agent, and |is| for the size of the largest information set in the CEGM.

Apath λ = q0q1q2 . . . is an infinite sequence of states such that there is a transition between each qi, qi+1. We use λ[i] to denote the ith position on path λ (starting from i = 0). The set of paths starting in q is denoted by Paths[M](q), and the set of their finite prefixes by Paths[M]fin (q).

A history h is a finite sequence of states. We use hF to denote its final state. Two histories h = q0q1 . . . qn and h′ = q′0 q′1 . . . q′n′ are indistinguishable for agent a (h ≈a h′ ) iff n = n′ and qi ∼a q′i for i = 1, . . . , n. Additionally, for any equivalence relation R over a set X we use [x]R to denote the equivalence class of x. Moreover, we use the abbreviations ∼A:= ⋃a∈A ∼a and ≈A:= ⋃a∈A ≈a. Note that relations ∼A and ≈A implement the "everybody knows" type of collective knowledge.

2.3 Semantic Variants of Strategic Ability

A number of semantic variations have been proposed for ATL, cf. e.g. [Jamroga, 2003; Schobbens, 2004; Jamroga and van der Hoek, 2004; ˚Agotnes et al., 2007; ˚Agotnes and Walther, 2009]. In this paper, we are concerned with the semantic variants ATLir and ATLiR [Schobbens, 2004].

The following types of strategies are used in the respective semantic variants:

• ir (imperfect information + imperfect recall): sa : St → Act s.t. sa(q) ∈ da(q) for all q, with the constraint that q ∼a q′ implies sa(q) = sa(q′ );
• iR (imperfect information + perfect recall): sa : St+ → Act s.t. sa(q0 . . . qn) ∈ da(qn) for all q0, . . . , qn, with the constraint that h ≈a h′ implies sa(h) = sa(h′ ).

That is, strategy sa is a conditional plan specifying a's actions in each state of the system (for memoryless agents) or for every possible history of the system evolution (for agents with perfect recall). Moreover, strategies specify the same choices for indistinguishable states (resp. histories). Collective strategies sA are tuples of individual strategies sa, one per a ∈ A.

The "objective outcome" function outo (q, sA) returns the set of all paths that may occur when agents A execute strategy sA from state q onward. The set of "subjectively possible outcomes" is defined as outi (q, sA) = ⋃q∼Aq′ out o (q′ , sA).

The semantics of ATLxy, parameterized by the notion of outcome (x ∈ {o, i}) and the type of recall (y ∈ {r, R}), can be given by the following clauses:

• M, q |=xy p iff q ∈ π(p), where p ∈ Π;
• M, q |=xy ¬ϕ iff M, q ̸ |=xy ϕ;
• M, q |=xy ϕ∧ψ iff M, q |=xy ϕ andM, q |=xy ψ;
• M, q |=xy 〈〈A〉〉Xϕ iff there is a collective iy-strategy sA such that, for each path λ ∈ outx (q, sA), we have M, λ[1] |=xy ϕ;
• M, q |=xy 〈〈A〉〉Gϕ iff there exists sA such that, for each λ ∈ outx (q, sA), we have M, λ[i] |=xy ϕ for every i ≥ 0;
• M, q |=xy 〈〈A〉〉ϕUψ iff there exists sA such that, for each λ ∈ outx (q, sA), there is i ≥ 0 for which M, λ[i] |=xy ψ, and M, λ[j] |=xy ϕ for each 0 ≤ j < i.

2.4 Known Complexity Results

In this paper, we focus on verifying MAS with imperfect information, i.e., on model checking ATLir and ATLiR. The former problem is known to be ∆P2 -complete [Schobbens, 2004; Jamroga and Dix, 2006]. 1 The latter problem is undecidable in general [Dima and Tiplea, 2011], but it becomes EXPTIME-complete when only singleton coalitions are allowed in the formula (the upper bound follows from [Guelev et al., 2011, Prop. 33], the lower bound from [Reif, 1984]). A brief summary of the results is presented in Figure 1; a more comprehensive overview can be found in [Bulling et al., 2010]. All the complexity results in this paper are given w.r.t. the number of transitions in the model and the length of the formula.

In contrast, model checking for perfect information strategies is much cheaper, namely P-complete [Alur et al., 2002].

3 Abilities of Single Agents: Imperfect Recall

Model checking agents with imperfect information is significantly harder than ones with perfect information. But what if the agents have almost perfect information, e.g., their information sets are of size at most 2? Or, symmetrically, they have almost no incoming information (say, all the states are split between only 2 information sets)? In this paper, we systematically study the subproblems generated by such assumptions. In the next two sections we look at the simpler case of individual abilities, i.e., when only singleton coalitions are allowed in the formulae. We refer to the fragment of ATL containing only such formulae as 1ATL. Later, in Section 5, we consider arbitrary coalitional strategies.

1 Where ∆P2 = PNP is the class of problems solvable in polynomial time by a deterministic Turing machine sending adaptive queries to an oracle for NP.

To help the reader navigate through the maze of formal arguments, we summarize our findings now. An outline of the main results is presented in Figure 2. On the one hand, we distinguish between agents playing memoryless strategies (i.e., 1ATLir) and agents with perfect recall (i.e., 1ATLiR). On the other hand, we look at models of almost perfect information (information sets of constant size, or bounded by a constant) and models of almost nil observability (constant number of information sets per agent). The cases with complexity lower than for the general problem are highlighted. As it turns out, if we consistently pair weak observability with weak recall, or almost perfect observability with perfect recall, model checking becomes easy. Interestingly, the complexity decreases also in the case of blindfold memoryful agents (essentially, agents who can only count).

3.1 Agents that Don't Miss Much (Small Info Sets)

ATLir is appealing in practice because it avoids overestimating the agents' epistemic capabilities, and at the same time yields the lowest verification complexity. We already mentioned that model checking for perfect information strategies is tractable. One would hope that, for agents with almost perfect information, the complexity is similarly low. Unfortunately, it turns out to be as hard as in the general case.

Theorem 1. Model checking 1ATLir over CEGMs with information sets of size at most 2 is ∆P2 -complete.

The proof relies on a translation T of models and formulae to be model-checked, so that each transition executing an action for agent 1 is split into a tree of transitions, with only doubleton information sets on the way. Moreover, there is a one-to-one correspondence between potentially successful uniform strategies for agent 1 in the new and the original model. In consequence, we get that M, q |=ir 〈〈1〉〉φ iff T (M), q |=ir T (〈〈1〉〉φ). We explain the translation now, and use it to complete the proof at the end of the subsection.

Formula Translation

Let ATL1U be the subset of ATL using only agent 1 in strategic operators and only the Until modality. We will modify the model by adding new states, hence we introduce a fresh proposition real to label the original states. Now, for each φ, φ′ ∈ ATL1U and p ∈ Π:

• T (p)=p, T (φ∧φ′ )=T (φ)∧T (φ′ ), T (¬φ)=¬T (φ),
• T (〈〈1〉〉φUφ′ )=〈〈1〉〉(real =⇒ T (φ))U(real∧T (φ′ )).

Model Translation: Idea

The transformation of models is more involved. Let M = 〈Agt, St,Π, π,Act, d, o〉 be a CEGM with at least twoagents, such that real ̸∈ Π. Let q0 ∈ St and Q = {q0}∼1 = {q0, q1, . . . , qk}, where k > 2. We build a model MQ that "simulates" the outgoing transitions in Q by a forest where |is| ≤ 2 and the strategic abilities of agent 1 remain the same.

For convenience, denote Acts = d1(q0) and introduce a new dummy action nop of agent 2. We also define a magic number H = (|Q| 2 ) × |Acts| · (|Acts| - 1), later used as the "height" of the structure that replaces Q after transformation. Now, for each qi ∈ Q and α ∈ Acts, define the set of new states qi, qα i , qαα i , . . . , qαH i , and denote Q′ = {qαn i | qi ∈ Q and 0 ≤ n ≤ H} (by convention, a0 = ϵ). We also introduce transitions qαn i (α,nop) -→ qαn+1 i for all 0 ≤ n < H. Moreover, we introduce a fresh state sink and put qαn i (β,γ) -→ sink, for all 0 < n ≤ H and γ ∈ d2(qi), where α ̸= β. Intuitively, for a given α ∈ Acts, once the transition labeled with α is selected in qi, the same action a needs to be executed until reaching qαH i if sink is to be avoided.

We now define the indistinguishability relation ∼∗ on Q′ for agent 1 as any equivalence relation on Q′ s.t. for each q ∈ Q′ we have |{q}∼∗ | ≤ 2 and for all qi, qj ∈ Q:

So far we have created a temporal-epistemic structure over the set Q′ ∪ {sink}. While this construction may seem involved, it serves a simple purpose. Observe that a uniform strategy for agent 1 can enforce a path from qi to qαH i only by repeatedly executing the action α ∈ Acts ; any deviation from choosing α is "punished" by an immediate transition to sink . Thus, the requirement of uniformity together with Condition (♣) yield that if qαH i is reached from qi and qαH j is reached from qj by the same strategy, then the strategy repeatedly executes the same action over both paths.

The selected value of H enables a construction that satisfies Condition (♣). An instance of the construction is shown in Fig. 3, where Q = {q0, q1, q2} and d1(q0) = {A, B}. The transitions to the sink state are omitted. The key to understanding the magic formula H is to notice that for each pair of states (hence the Newton symbol) we discern each pair of different actions by adding a new level to the tower in Fig. 3.

Model Translation: Formal Construction

The CEGM MQ = 〈Agt, St′ , Π′ , π′ , Act ∪ {nop}, d′ , o′ 〉 is defined by:

• St′ = (St \ Q) ∪ Q′ ∪ {sink} and Π′ = Π ∪ {real};
• π′ (q) = π(q) ∪ {real} for all q ∈ St and π′ (q) = ∅ for the remaining states;
• the new protocol:
• d′i (q) = di(q), for all q ∈ St \ Q and i ∈ {1, 2} (the inherited protocol),
• d′1 (qαn ) = d1(q) for all qαn ∈ Q′ ,
• d′2 (qαH ) = d2(q) for each qαH ∈ Q′ ,
• d′i (q) = {nop} otherwise, where i ∈ {1, 2};

1

Figure 3: Enforcing uniformity for action A.

• the new transition function:

Note that all the states copied fromM are labeled with real. The new transition function o′ behaves as follows: (1) if an action is executed in a state q outside of Q′ , then the outcome is the same as for o; (2) if q = qi ∈ Q′ and q ̸= qαH i , then agent 1 is in control and can decide to either execute α and move towards qαH i or dive in sink; (3) if q = qαH i , then agent 2 regains its part of control.

Finally, we define the indistinguishability relation ∼′1 of agent 1 over MQ by requesting that q ∼′1 q′ iff q, q′ ∈ St \Q and q ∼1 q′ or q, q′ ∈ Q′ and q ∼∗ q′ .

We can now define the final translation T (M) of CEGM M. Namely, T (M) is obtained by an iterative reduction of all information sets of size greater than 2 until there are none.

The construction preserves enforceability for agent 1 on the set of objective outcome paths:

Proof sketch. The proof follows by induction on structure of φ. It is sufficient to prove the thesis for a single step of reduction, i.e., MQ instead T (M). We omit the details of a rather tedious but not difficult proof due to lack of space.

We can now proceed to the proof of Theorem 1.

Proof sketch. We only need to show ∆P2 -hardness. The method used to this end in [Jamroga and Dix, 2006] is based on a reduction of SNSAT2 [Laroussinie et al., 2001] to model checking of certain ATLir formulae over two-player CEGMs. Namely, a set F of propositional formulae in CNF is given as an instance of SNSAT2, and each of them is translated into a CEGM component in a satisfiability-encoding manner, see [Jamroga and Dix, 2006, Sec. 3.1 and Fig. 2].

The resulting model is denoted by M∆. In [Jamroga and Dix, 2006, Theorem 4], a formula Φ∆ ∈ ATLir is proposed such that F is satisfiable iff M∆ |=ir Φ∆. The formula contains the "Next" operator, but it can be easily replaced by "Until" to obtain a satisfiability-preserving formula Φ′∆ ∈ ATL1U . Moreover, on M∆, the or and ir semantics of Φ′∆ coincide. The same applies to their translations T (M∆) and T (Φ′∆). Thus, by Theorem 2 we get that SNSAT2(F) iff M∆ |=ir Φ′∆ iff M∆ |=or Φ′∆ iff T (M∆) |=or T (Φ′ ) iff T (M∆) |=ir T (Φ′ ). All the transformations can be done in polynomial time w.r.t. the size of the inputs.

3.2 Agents that Don't See Much (Few Info Sets)

For memoryless agents with limited observational capabilities, model checking becomes easy.

Theorem 3. Let k be a constant. Model checking 1ATLir over the class of CEGMs with #is ≤ k is P-complete.

Proof. The lower bound follows from P-completeness of 1ATLIr [Alur et al., 2002]. For the upper bound, observe that each agent has only O(|Act|k ) available strategies, and one can determine if a given strategy is winning in linear time by CTL model checking. Thus, we can check the strategies one by one in deterministic polynomial time.

4 Abilities of Single Agents: Perfect Recall

We continue the analysis from the previous section, now turning to specifications in 1ATLiR.

4.1 GoodMemory, Agents that Don't Miss Much

Model checking of agents with perfect recall and almost perfect information also becomes easy.

Theorem 4. Let k be a constant. Model checking 1ATLiR over CEGMs with |is| ≤ k is P-complete.

Proof. The lower bound follows from P-completeness of 1ATLIR [Alur et al., 2002]. For the upper bound, we use the construction in [Guelev et al., 2011, Section 6] that translates model checking of 1ATLiR in CEGM M to verification of perfect information strategies in a CGS M ′ . Note that the number of transitions in the new model is |M ′ | = O(|M| · 2|is| ) ≤ O(|M| · 2k ) = O(|M|). Moreover, model checking for perfect information can be done in polynomial time w.r.t. the size of the model and the formula.

4.2 GoodMemory, Agents that Don't See Much

Consider now the case of models with few information sets.

Theorem 5. Model checking 1ATLiR over CEGMs with at most 2 information sets per agent is EXPTIME-complete.

The inclusion is straightforward from [Guelev et al., 2011, Prop. 33]. To obtain the lower bound, we develop a reduction from model checking CEGMs with arbitrarily many observations to CEGMs with only two available observations, modeled by the "white" and the "dark" states. The idea is that, for a transition q -→ q′ , the observation provided by the target state q′ is simulated by a sequence of intermediate "dark" and "white" states, signalling in binary the index of the original information set [q′ ].

Model Translation

Let M = 〈Agt, St,Π, π,Act, d, o〉 be a CEGM and n = |St/∼1| be the number of information sets for agent 1 ∈ Agt. We label the information sets of ∼1 with ordinals from 0 to n - 1. Let ctr(q) be the index of [q]∼1 . Moreover, ctri(q) denotes the ith bit of binary representation of ctr(q), for 0 ≤ i ≤ ⌈log n⌉.

For any transition q γ -→ q′ in M, we introduce 2⌈logn⌉ fresh states F = {qγ,0 i , qγ,1 i }⌈logn⌉ i=0 and the usual sink state. We use the states in F to encode ctr(q) and ctr(q′ ). Namely, we replace q γ -→ q′ with the following sequence:

where ⋆ should be replaced with the bundle of all possible actions for the grand coalition, i.e., Act |Agt| . This process is repeated for each transition in M. We will denote part (2) of the sequence by enc(q), and part (3) by enc ′ (q′ ).

In the next stage we unify the protocol for agent 1 by firstly adding the usual fresh sink state and adding for each action α ∈ Act \ d1(q) and β ∈ dAgt\{1}(q) a new transition q (α,β) -→ sink. Intuitively, agent 1 is punished for not following the original protocol by a transition to sink. We also copy the labeling of q to all the intermediate states ˆ q ∈ F, i.e., q ∈ π(p) iff ˆ q ∈ π(p) for all p ∈ Π.

Finally, we add the indistinguishability relation for agent 1 as follows: (1) the original states from St, sink, and {qγ,0 i }⌈logn⌉ i=0 are colored grey; (2) the states from {qγ,1 i }⌈logn⌉ i=0 are colored white; (3) we assume that agent 1 can observe only the color of a state. The resulting CEGM is denoted by T e (M).

We illustrate the construction in Fig. 4. In the example, there is only one agent, and states q, q′ belong to two information sets with ctr(q) = 10bin and ctr(q′ ) = 11bin. Moreover, Act = {A, B} and d1(q) = {A}.

Theorem 6. For ATLiR formulae 〈〈A〉〉γ containing no nested strategic modalities and no operator X, we have: M, q |=iR 〈〈A〉〉γ ⇐⇒ T e (M), q |=iR 〈〈A〉〉γ.

Proof sketch. For simplicity let A = {1}. The proof of the general case differs only in the number of the fresh states used to encode the observations of the protagonist coalition. A possible scheme of such encoding can be based on enumerating the information sets of each i ∈ A with functions ctr i (·). Then, each transition q γ -→ q′ is swapped with its replacement, where the agents of the coalition take turns in a fixed order to enforce the encoding of source and target information sets using separate fresh locations. These locations are created and labeled as in the single-agent above.

We establish a correspondence between iR-strategies over M and T e (M) that preserves U and G. Let λ = q0q1 . . . qk be a history in M. By lft(λ) = q0enc(q0)enc ′ (q1)q1 . . . enc(qk-1)enc ′ (qk)qk we denote the lifting of λ to T e (M). Note that by construction each finite history in T e (M) is of form λ′ = q0enc(q0)enc ′ (q1)q1 . . . enc(qk-1)enc ′ (qk)qkR, where R is a sequence containing only fresh states. We can thus define the casting of λ′ to M as cst(λ′ ) = q0q1 . . . qk.

Now, let s1 be an iR-strategy for agent 1, over M. We define the lifting lft(s1) of s1 to T e (M) as a function s.t. lft(s1)(λ′ ) = s1(cst(λ′ )) for all the histories λ′ over T e (M) such that λ′ [0], λ′F ̸∈ F and lft(s1)(λ′ ) = B for a fixed B ∈ Act for all the remaining histories. Intuitively, lft(s1) makes the same choices as s1, unless the path reaches a fresh state where the fixed action is used.

Let s′1 be an iR-strategy for agent 1, over T e (M). The casting cst(s′1 ) of s′1 to M is a function s.t. cst(s′1 )(λ) = s′1 (lft(λ)) for each history λ over M. Intuitively, cst(s′1 ) makes the same choices as s′1 while ignoring the fresh states.

To conclude the proof, it is easy to see that s1 enforces p along each path starting from q iff lft(s1) does so. Moreover, it is routine to show that the uniformity is preserved, i.e., lft(s1) and cst(s′1 ) as defined above are iR-strategies.

The lower bound in Theorem 5 follows from Theorem 6 and the EXPTIME-hardness of solving reachability games with imperfect information [Reif, 1984].

4.3 Special Case: Blindfold Agents with Recall

Two information sets are enough to make model checking ATLiR as hard as in arbitrary models. What happens if there is only a single information set, comprising of the whole state space? Such CEGMs are called blindfold. Note that, in blindfold CEGMs, memoryful strategies for any A ⊆ Agt can be interpreted as functions σA : N → Act, where σA(i) is the joint action selected by A in the ith step. Moreover, the set of the outcome paths of σA does not depend on the initial state, so one can as well write out(σA) instead of out(q, σA).

Interestingly, model checking ATLiR over blindfold CEGMs is easier than in the general case.

Theorem 7. Model checking ATLiR over the class of blindfold CEGMs is in PSPACE.

Proof. It suffices to show that 〈〈A〉〉pUr and 〈〈A〉〉Gp can be verified in PSPACE, where A ⊆ Agt and p, r ∈ Π. The idea is as follows: firstly we show that if these properties are true, then they can be attained by using finite strategies with memory that needs to cover only all the possible subsets of the state space. Secondly, we use this limit to build a model checker in a form of a non-deterministic Turing machine.

Let us start with q |= 〈〈A〉〉pUr and let σA : N → Act A be a joint strategy for A s.t. λ |= pUr for each λ ∈ out(σA). For each i ∈ N we inductively define the set Ai as follows: A0 = St \ [[r]] and Ai+1 = {states reachable in one step from Ai via σA} \ [[r]] for i > 0.

It follows from the definition of the Until modality that there exists the smallest index kfin ∈ N s.t. Ai = ∅ for all i ≥ kfin. Now, let us select any B ∈ {Ai}kfin i=0 and let kmin, kmax ∈ N be the minimal and maximal, resp., indices s.t. Akmin = B = Akmax . If kmin < kmax , then we can transform σA into σB A as follows: σB A (i) = σA(i) for all 0 ≤ i < kmin and σB A (i) = σA(i + kmax - kmin) for all i ≥ kmin. It is easy to see that λ |= pUr for each λ ∈ out(σB A ). The process of recomputing the sets {Ai}i∈I and further reducing the working strategy can be repeated until no reduction is possible, i.e., the family {Ai}i∈I contains no repetitions. This in turn means that I ≤ 2|St| and kfin ≤ 2|St| . Therefore, there exists a joint strategy for A that enforces pUr in less than 2|St| steps.

The construction for 〈〈A〉〉Gp follows analogously.

To build a non-deterministic Turing machine for 〈〈A〉〉p U r and 〈〈A〉〉Gp, we equip it with a deterministic |St|-bit counter that enables to track the progress of execution up to 2|St| steps. The machine consecutively guesses joint actions for A for the current step indicated by the counter, executes them and then increments the counter. Only recently reached states are preserved. The machine rejects if the counter exceeds 2|St| or a state violating the verified property has been reached. It accepts if while traversing along p-labeled states a state labeled with r has been reached along each path (the case of pU r) or a loop has been detected (the case of Gp).

5 Abilities of Coalitions

In Sections 3 and 4, we focused on formulae containing only singleton coalitions. We now briefly wrap up the study, presenting analogous results for multi-player teams. A summary is shown in Figure 5; again, the cases with lower complexity than for the general problem are highlighted.

We observe that, for models with small information sets, ∆P2 -completeness follows from Theorem 1 and the complexity of the general problem [Schobbens, 2004; Jamroga and Dix, 2006]. Moreover, Theorem 7 (inclusion in PSPACE for blindfold agents) is formulated and proved for the whole language of ATLiR. Finally, our reduction in Theorem 6 works also for coalitional abilities. Thus, model checking ATLiR for #is = k and k ≥ 2 is undecidable. 2

The last case that we address is that of coalitional abilities for memoryless agents with weak observational capabilities.

Theorem 8. Model checking ATLir over CEGMs with at most 2 information sets per agent is ∆P2 -complete.

Proof sketch. We adapt the ∆P2 -hardness proof in [Jamroga and Dix, 2006] by using a team of verifiers V = {v1 0 , . . . , vn∗m 0 , v1, . . . , vk} where n is the number of nested queries, m is the maximal number of clauses per query and k is the number of propositional variables in the instance of SNSAT2. Each agent vi0 controls the choice of the literal in a particular clause, and each agent vj controls the valuation of the Boolean variable underlying "her" literal. Every agent can only distinguish between the states she controls and the rest of the state space. Finally, we replace each occurrence of 〈〈v〉〉 with 〈〈V 〉〉 in the formula from [Jamroga and Dix, 2006], and the reduction goes through.

2 Alternatively, one can observe that the undecidability proof in [Dima and Tiplea, 2011] actually uses a model with #is = 2.

Note that the above proof requires that the number of agents in the class of models is variable (and is a parameter of the model checking problem). As it turns out, the requirement is essential for Theorem 8 to hold. This is especially important, as a fixed finite set of agents is often assumed beforehand, when defining the syntax of the agent logic. In those cases, model checking agents with limited epistemic capabilities is easy even in the coalitional case.

Theorem 9. Let k, n be constants. Model checking ATLir over the class of CEGMs with at most n agents and at most k information sets per agent is P-complete.

Proof. Straightforward extension of the proof of Theorem 3 (the number of coalitional strategies is now polynomial).

6 Conclusions

Verification of autonomous agents in multi-agent systems is an important research path. Despite some recent advances [Huang and van der Meyden, 2014; Pilecki et al., 2014; Busard, 2017; Jamroga et al., 2017], the problem is still open due to its inherent computational complexity. In this paper, we show that the complexity is in fact lower than expected in some borderline cases, in particular for agents with consistently good (resp. weak) observational and mental capabilities. We also show that, for agents whose capabilities are "in between," the problem is as hard as in the general case.

An interesting question for the future concerns the corresponding complexity results for ATL∗ . We would also like to establish the model checking complexity for coalitions with perfect recall and almost perfect information.

Acknowledgements

The authors acknowledge the support of the National Centre for Research and Development, Poland (NCBR), and the Luxembourg National Research Fund (FNR), under the PolLux/FNR-INTER project VoteVerif (POLLUXIV/1/2016).