--- title: "Some Things are Easier for the Dumb and the Bright Ones (Beware the Average!)" authors: - "Wojciech Jamroga" - "Michał Knapik" doi: "10.24963/ijcai.2019/240" url: "https://ijcai.org/proceedings/2019/240" pdf: "https://ijcai.org/proceedings/2019/0240.pdf" venue: "Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence" year: 2019 pages: "1734-1740" track: "Main track" keywords: - "Agent-based and Multi-agent Systems: Agent Theories and Models" - "Agent-based and Multi-agent Systems: Formal Verification, Validation and Synthesis" - "Knowledge Representation and Reasoning: Computational Complexity of Reasoning" --- # Some Things are Easier for the Dumb and the Bright Ones (Beware the Average!) Wojciech Jamroga, Michał Knapik *Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence*, pages 1734-1740. DOI: [10.24963/ijcai.2019/240](https://doi.org/10.24963/ijcai.2019/240) ## Abstract Model checking strategic abilities in multi-agent systems is hard, especially for agents with partial observability of the state of the system. In that case, it ranges from NP-complete to undecidable, depending on the precise syntax and the semantic variant. That, however, is the worst case complexity, and the problem might as well be easier when restricted to particular subclasses of inputs. In this paper, we look at the verification of models with "extreme" epistemic structure, and identify several special cases for which model checking is easier than in general. We also prove that, in the other cases, no gain is possible even if the agents have almost full (or almost nil) observability. To prove the latter kind of results, we develop generic techniques that may be useful also outside of this study. ## Full text ## 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. Figure 1: Existing complexity results | | Single agents | Coalitions | |----------------|------------------|---------------| | Memoryless | ∆P2 -complete | ∆P2 -complete | | Perfect recall | EXPTIME-complete | undecidable | 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. Figure 2: Model checking complexity for abilities of single agents | Single agents | Small info sets (|is| ≤ const) | Few info sets (#is ≤ const) | |-----------------|--------------------------------------------|----------------------------------------------| | Memoryless | I∆P2 -complete | P-complete | | Perfect recall | P-complete | in PSPACE for #is = 1 EXPTIME-c. for #is > 1 | 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}; ![Image](https://ijcai.org/proceedings/2019/fulltext/240/image_000000_c925551fdc897fe239a0cd958cfbd2537511983c713953d17ccb4c59c004517c.png) 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′ ]. Figure 4: Reducing the number of information sets for a single agent ![Image](https://ijcai.org/proceedings/2019/fulltext/240/image_000001_9f0883aa1d73eb291e9a5d7537d29093458c376d674e563e512c563431a1adbd.png) ## 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. Figure 5: Model checking complexity for abilities of coalitions | Coalitions | Small info sets (|is| ≤ const) | Few info sets (#is ≤ const) | |----------------|--------------------------------------------|-----------------------------------------------| | Memoryless | ∆P2 -complete | IP-compl./∆P2 -compl. | | Perfect recall | ? | in PSPACE for #is = 1 undecidable for #is > 1 | 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). ## References 1. [Ågotnes and Walther, 2009] T. Ågotnes and D. Walther. A logic of strategic ability under bounded memory. Journal of Logic, Language and Information, 18(1):55-77, 2009. 2. [Ågotnes et al., 2007] T. Ågotnes, V. Goranko, and W. Jam- roga. Alternating-time temporal logics with irrevocable strategies. In Proceedings of TARK XI, pages 15-24, 2007. 3. [Ågotnes et al., 2015] T. Ågotnes, V. Goranko, W. Jamroga, and M. Wooldridge. Knowledge and ability. In H.P. van Ditmarsch, J.Y. Halpern, W. van der Hoek, and B.P. Kooi, editors, Handbook of Epistemic Logic, pages 543-589. College Publications, 2015. 4. [Alur et al., 2002] R. Alur, T. A. Henzinger, and O. Kupfer- man. Alternating-time Temporal Logic. Journal of the ACM, 49:672-713, 2002. 5. [Belardinelli et al., 2017] F. Belardinelli, A. Lomuscio, A. Murano, and S. Rubin. Verification of multi-agent sys- tems with imperfect information and public actions. In Proceedings of AAMAS, pages 1268-1276, 2017. 6. [Berwanger and Kaiser, 2010] D. Berwanger and L. Kaiser. Information tracking in games on graphs. Journal of Logic, Language and Information, 19(4):395-412, 2010. 7. [Berwanger et al., 2018] D. Berwanger, A. B. Mathew, and M. van den Bogaard. Hierarchical information and the synthesis of distributed strategies. Acta Inf., 55(8):669- 701, 2018. 8. [Bulling et al., 2010] N. Bulling, J. Dix, and W. Jamroga. Model checking logics of strategic ability: Complexity. In M. Dastani, K. Hindriks, and J.-J. Meyer, editors, Spec- ification and Verification of Multi-Agent Systems, pages 125-159. Springer, 2010. 9. [Busard, 2017] S. Busard. Symbolic Model Checking of Multi-Modal Logics: Uniform Strategies and Rich Expla- nations. PhD thesis, Universite Catholique de Louvain, 2017. 10. [Chatterjee et al., 2007] K. Chatterjee, L. Doyen, T.A. Hen- zinger, and J.-F. Raskin. Algorithms for omega-regular games of incomplete information. Logical Methods in Computer Science, 3(3), 2007. 11. [Dima and Tiplea, 2011] C. Dima and F.L. Tiplea. Model- checking ATL under imperfect information and perfect recall semantics is undecidable. CoRR, abs/1102.4225, 2011. 12. [Doyen and Raskin, 2011] L. Doyen and J.-F. Raskin. Games with imperfect information: Theory and algo- rithms. In Lecture Notes in Game Theory for Computer Scientists, pages 185-212. Cambridge University Press, 2011. 13. [Guelev et al., 2011] D.P. Guelev, C. Dima, and C. Enea. An alternating-time temporal logic with knowledge, perfect recall and past: axiomatisation and model-checking. Jour- nal of Applied Non-Classical Logics, 21(1):93-131, 2011. 14. [Huang and van der Meyden, 2014] X. Huang and R. van der Meyden. Symbolic model checking epistemic strategy logic. In Proceedings of AAAI Conference on Artificial Intelligence, pages 1426-1432, 2014. 15. [Jamroga and Dix, 2006] W. Jamroga and J. Dix. Model checking ATL ir is indeed ∆ P 2 -complete. In Proceedings of EUMAS, volume 223 of CEUR Workshop Proceedings, 2006. 16. [Jamroga and van der Hoek, 2004] W. Jamroga and W. van der Hoek. Agents that know how to play. Fundamenta Informaticae, 63(2-3):185-219, 2004. 17. [Jamroga et al., 2017] W. Jamroga, M. Knapik, and D. Kurpiewski. Fixpoint approximation of strategic abilities under imperfect information. In Proceedings of the 16th International Conference on Autonomous Agents and Multiagent Systems (AAMAS), pages 1241-1249. 18. IFAAMAS, 2017. 19. [Jamroga, 2003] W. Jamroga. Some remarks on alternat- ing temporal epistemic logic. In B. Dunin-Keplicz and R. Verbrugge, editors, Proceedings of Formal Approaches to Multi-Agent Systems (FAMAS 2003), pages 133-140, 2003. 20. [Laroussinie et al., 2001] F. Laroussinie, N. Markey, and Ph. Schnoebelen. Model checking CTL+ and FCTL is hard. In Proceedings of FoSSaCS'01, volume 2030 of Lecture Notes in Computer Science, pages 318-331. Springer, 2001. 21. [Maubert and Murano, 2018] Bastien Maubert and Aniello Murano. Reasoning about knowledge and strategies un- der hierarchical information. In Proceedings of KR, pages 530-540, 2018. 22. [Peterson and Reif, 1979] G. Peterson and J. Reif. Multiple- person alternation. In Proceedings of the 20th Annual Symposium on Foundations of Computer Science (FOCS), pages 348-363. IEEE Computer Society Press, 1979. 23. [Pilecki et al., 2014] J. Pilecki, M.A. Bednarczyk, and W. Jamroga. Synthesis and verification of uniform strate- gies for multi-agent systems. In Proceedings of CLIMA XV, volume 8624 of Lecture Notes in Computer Science, pages 166-182. Springer, 2014. 24. [Reif, 1984] John H. Reif. The complexity of two-player games of incomplete information. J. Comput. Syst. Sci., 29(2):274-301, 1984. 25. [Schewe and Finkbeiner, 2007] S. Schewe and B. Finkbeiner. Distributed synthesis for alternating- time logics. In Proceedings of ATVA, volume 4762 of Lecture Notes in Computer Science, pages 268-283. 26. [Schobbens, 2004] P. Y. Schobbens. Alternating-time logic with imperfect recall. Electronic Notes in Theoretical Computer Science, 85(2):82-93, 2004. 27. [van der Hoek et al., 2006] W. van der Hoek, A. Lomuscio, and M. Wooldridge. On the complexity of practical ATL model checking. In Proceedings of International Joint Conference on Autonomous Agents and Multiagent Sys- tems (AAMAS), pages 201-208. ACM, 2006.