Making Agents' Abilities Explicit

Alternating-time temporal logics (ATL/ATL*) represent a family of modal logics for reasoning about agents' strategic abilities in multiagent systems (MAS). The interpretations of ATL/ATL* over the semantic model Concurrent Game Structures (CGS) usually vary depending on the agents' abilities, for instance, perfect vs. imperfect information, perfect vs. imperfect recall, resulting in a variety of variants which have been studied extensively in literature. However, they are defined at the semantic level, which may limit modeling flexibilities and may give counter-intuitive interpretations. To mitigate these issues, in this work, we propose to extend CGS with agents' abilities and study the new semantics of ATL/ATL* under this model. We give PSACE/2EXPTIME model-checking algorithms for ATL/ATL* and implement them as a prototype tool. Experiment results show the practical feasibility of the approach.


Introduction
Multiagent systems (MAS) consisting of multiple autonomous agents are a wide adopted paradigm of intelligent systems. Game-based models and associated logics, as the foundation of MAS, have received tremendous attention in recent years. The seminar work [Alur et al., 2002] proposed concurrent game structures (CGS) as the model of MAS and alternating-time temporal logics (typically ATL and ATL * ) as specification languages for expressing temporal goals. In a nutshell, a CGS consists of multiple players which are used to represent autonomous agents, components and the environment. The model describes how the MAS evolves according to the collective behavior of agents. ATL/ATL * , an extension of the Computational Tree Logics (CTL/CTL * ), features coalition modality A . The formula A ϕ expresses the property that the coalition (i.e. the agent group) A has a collective strategy to achieve a certain goal specified by ϕ.
A series of extensions of ATL-like logics have been studied which take different agents' abilities into account. These abilities typically include whether the agents can identify the current state of the system completely or only partially (perfect vs. imperfect information), and whether the agents can memorize the whole history of observations or simply part of them (perfect vs. imperfect recall). Different abilities usually induce distinct semantics of logics, which are indeed necessary because of the versatility of problem domains. These semantic variants and their modelchecking problems comprise subjects of active research for almost two decades, to cite a few [Schobbens, 2004;Jamroga and van der Hoek, 2004;Ågotnes et al., 2007;Dima and Tiplea, 2011;Bulling and Jamroga, 2011;Laroussinie and Markey, 2015].
While the agents' abilities play a prominent role [Bulling and Jamroga, 2014], the semantics of ATL-like logics only refers to them implicitly. In other words, the logic per se does not specify what ability an agent has; instead one can infer the ability an agent requires by examining the goal specified in the logic. This approach, being elegant and valuable to understand the relationship between different abilities, suffers from a few shortcomings: (1) From the modelling perspective, it is common in practice that agents in an MAS vary in their abilities (for instance, agents modeling sensors may not identify the complete state of system so can only use strategies with imperfect information). When building up a model, these abilities ought to be encoded explicitly. Such modeling flexibility is not supported by existing formalisms. (2) From the semantic perspective, ATL-like logics may exhibit some counter-intuitive semantics. A ϕ is interpreted as the coalition A has a collective strategy to achieve the goal ϕ "no matter what the other agents do" rather than "no matter which strategies the other agents choose", hence, neglects the (multi-player) game nature in the evolution of MAS. For instance, when it comes to the imperfect information/recall setting, only agents in the formula A ϕ are assumed to use imperfect information/recall strategies, while the agents not in A may still use perfect information and perfect recall strategies. Even worse, if the coalition modalities are nested, the same agent may have different abilities to fulfill the objectives specified in different sub-formulae, which results in inconsistency. This phenomenon has also been mentioned in [Mogavero et al., 2014;Cermák et al., 2014] which proposed a strategic logic does make explicit references to strategies of all agents including those not in A. However, all agents in strategic logic should have same abilities.
To summarize, it occurs to us that the current approach in which the temporal formulae are with implicit agents' abilities at the semantics level impedes necessary modeling flexibility and often yields unpleasant (even weird) semantics. Instead, we argue that coupling agents' abilities at the syntactic level of system models would deliver a potentially better approach to overcome the aforementioned limitations. Bearing the rationale in mind, we propose a new MAS model, named Agents' Abilities Augmented Concurrent Game Structures (ACGS), which encompasses agents' abilities explicitly. We investigate ATL/ATL * over ACGS. We show that in general the new semantics of ATL/ATL * over ACGS is incomparable with others even if the underlying CGS models are the same. We also study the model-checking problem of ATL/ATL * over ACGS. We show that this problem is generally undecidable, as the problem of ATL over CGS under the imperfect information and perfect recall setting is already undecidable [Dima and Tiplea, 2011]. However, we manage to show that the model-checking problem for ATL * (resp. ATL) on ACGS is 2EXPTIME-complete (resp. in PSPACE) when the imperfect information and perfect recall strategies are disallowed. We implement our algorithms in a prototype tool and conduct experiments on some standard applications from the literature. The results confirm the feasibility of our approach.
The source code of our tool is available at [MCMAS-ACGS, 2018] which also includes some further experiments and comparison of ATL/ATL * semantics between CGS and ACGS.

Concurrent Game Structures
Given an infinite word ρ = s 0 s 1 . . ., we denote by ρ j the symbol s j , ρ [0.. j] the prefix s 0 . . . s j , and ρ [ j..∞] the suffix s j s j+1 . . .. Given a finite word ρ = s 0 s 1 · · · s m , we denote by ρ j the symbol s j for 0 ≤ j ≤ m, and lst(ρ) the symbol s m .
Let AP denote a finite set of atomic propositions. A concurrent game structure (CGS) is a tuple G (S , S 0 , Ag, (Ac i ) i∈Ag , (∼ i ) i∈Ag , (P i ) i∈Ag , ∆, λ), where S is a finite set of states; S 0 ⊆ S is a set of initial states; Ag = {1, ..., n} is a finite set of agents; Ac i is a finite set of local actions of agent i; ∼ i ⊆ S × S is an epistemic accessibility relation (an equivalence relation); P i : S → 2 Ac i is a protocol function such that P i (s) = P i (s ′ ) for every s ∼ i s ′ ; ∆ : S × Ac → S is a transition function with Ac = i∈Ag Ac i being a set of joint actions; and λ : S → 2 AP is a labeling function which assigns each state with a set of atomic propositions. Given a joint action a = a 1 , ..., a n ∈ Ac, we use a(i) to denote the local action of agent i in a.
Intuitively, i (resp. I) signals that agents can only observe partial information characterized via epistemic accessibility relations (resp. complete information with all epistemic accessibility relations being the identity relation), while r (resp. R) signals that agents can make decision based on the current observation (resp. the whole history of observations). We will, by slightly abusing notation, extend Ir-strategies and ir-strategies θ i to the domain S + such that for all ρ ∈ S + , θ i (ρ) = θ i (lst(ρ)). We denote by Θ σ i for σ ∈ {Ir, IR, ir, iR} the set of σ-strategies for agent i.

Outcomes.
A collective σ-strategy of a set of agents A is a function υ σ A assigning each agent i ∈ A with a σ-strategy υ σ A (i) ∈ Θ σ i . For i ∈ A and ρ ∈ S + , we denote the local action υ σ A (i)(ρ) of agent i by υ σ A (i, ρ), and the set Ag \ A by A. Given a state s, two collective σ/σ ′ -strategies υ σ A and υ σ ′ A yield a path ρ, denoted by play(s, υ σ For every state s ∈ S and collective σ-strategy υ σ A of A, the outcome function is defined as follows: i.e., the set of all possible plays that may occur when each agent i ∈ A enforces its σ-strategy υ σ A (i) from the state s. The subscript G is dropped in O σ G when it is clear from the context.

Alternating-Time Temporal Logics
The alternating-time temporal logic ATL/ATL * is an extension of the branching-time logic CTL/CTL * by replacing the existential path quantifiers E with coalition modalities A [Alur et al., 2002]. Intuitively, the formula A φ expresses that the set of agents A has a collective strategy to achieve the goal φ no matter which strategies the agents in A choose. Formally, ATL * is defined by the following grammar: where ϕ (resp. φ) denotes state (resp. path) formulae, q ∈ AP and A ⊆ Ag.
The derived operators are defined as usual: An LTL formula is an ATL * path formula by restricting ϕ to atomic propositions.
The semantics of ATL * is traditionally defined over CGS. When agents's abilities are considered, it is often parameterized with a strategy type σ ∈ T str , denoted by ATL * σ [Bulling and Jamroga, 2014]. Formally, let G be a CGS and s be a state of G, the semantics of ATL * σ (i.e. the satisfaction relation) is defined inductively as follows: (where ̺ is a state s or path ρ) • G, s | = σ q iff q ∈ λ(s); • G, s | = σ A φ iff there exists a collective σ-strategy υ σ A of agents A such that ∀ρ ∈ O σ (s, υ σ A ), G, ρ | = σ φ; • G, ρ | = σ ϕ iff G, ρ 0 | = σ ϕ; Vanilla ATL. ATL is a sublogic of ATL * where each occurrence of the coalition modality A is immediately followed by a temporal operator. Formally, ATL is defined by the following grammar: Remark that the operator R cannot be defined using other operators in ATL with imperfect information [Laroussinie et al., 2008], so is included for completeness.
Given an ATL * formula ϕ, a CGS G and a strategy type σ ∈ T str , the model-checking problem is to determine whether G, s | = σ ϕ or not, for each initial state s of the CGS G.
Some Semantic Issues. We observe that the semantics of ATL/ATL * refers to the agents' abilities in an implicit manner. For the formula A ϕ, the specified σ-strategies only apply to agents in A while the agents in A could still choose beyond σ-strategies (e.g. IR-strategies). In other words, A has a collective σ-strategy to achieve ϕ no matter what the other agents do. When σ is IR as in the original work by [Alur et al., 2002], this interpretation of A ϕ is plausible, as "no matter what the other agents do" is effectively the same as "no matter which strategies the other agents choose". However, when σ is set to be more restricted than IR, agents not in A are still allowed to use IR-strategies.
As mentioned in the introduction, this results in a few shortcomings. From a modeling perspective, arguably agents' abilities should be decided by the practical scenario. Namely, they should be fixed when the model is built, and all agents stick to their respective abilities independent of logic formulae. More concretely, from the semantic perspective, the existing semantics does not take into account the abilities of agents who are not in A, and neglects the (multi-player) game nature in the evolution of MAS. As a result, it may exhibit some counter-intuitive semantics. For instance, consider two formulae A φ and A ′ φ ′ such that agent i ∈ A \ A ′ , i may have different abilities to achieve φ and φ ′ . Let us consider an autonomous road vehicle scenario to see why this is not ideal. There are several autonomous cars which can only observe partial information and have bounded memory. An MAS model G consists of agents in A modeling autonomous cars, and an additional environment agent e. We can reasonably assume that all the car agents use ir-strategies, while e uses IR-strategies. The property A ′ φ expresses that autonomous cars A ′ ⊂ A can cooperatively achieve the goal φ no matter what strategies the other cars and the environment choose. Verifying that G satisfies A ′ φ under the existing semantics would allow car agents A\A ′ to use IR-strategies. If G satisfies A ′ φ, then the result is conclusive, i.e., A ′ φ holds for the system. However, if G invalidates A ′ φ, we cannot deduce that A ′ φ fails because we overestimate the abilities of agents in A \ A ′ when evaluating A ′ φ. In other words, for the formula A ϕ under | = σ where σ IR, it seems to be inappropriate to render the agents not in A extra powers of IR to potentially defeat agents from A when their abilities are actually much weaker.

Agents' Abilities Augmented Concurrent Game Structures
In this section, we introduce agents' abilities augmented concurrent game structures (ACGS in short), which explicitly equip each agent with a strategy type from T str . As such, agents have fixed abilities throughout their lives for a given CGS. Formally, an ACGS is a pair M (G, π), where G is a CGS and π : Ag → T str is a function that assigns a strategy type π(i) to the agent i. We assume that, for each agent i ∈ Ag with π(i) ∈ {IR, Ir}, ∼ i is an identity relation, as agents with perfect information should be able to distinguish two distinct states. Paths of M are defined the same as for the CGS G, but strategies and outcomes of M have to be redefined as follows.

Strategies and Outcomes. Let A be a set of agents. A collective strategy of
Given a state s ∈ S , for every collective strategy ξ A of the set A of agents, the outcome O M (s, ξ A ) of M is the set of all possible paths that may occur when each agent i ∈ A enforces its π(i)-strategy ξ A (i) from state s, and other agents i ∈ A can only choose π(i)-strategies instead of general IR-strategies.
Semantics of ATL/ATL * . The difference of outcomes between ACGS and CGS induces a distinct semantics of ATL * on ACGS than CGS. Let M be an ACGS and s be a state in M, the semantics of ATL * on M is defined similar to the one on CGS, except that the semantics of the state formulae of the form A φ is defined as follows: Remark that this semantics takes into account whether the agents from A have perfect or imperfect information/recall. Given an ACGS M and an ATL/ATL * formula ϕ, the model-checking problem is to determine whether M, s | = ϕ holds, for every initial state s of G. Given a state formula ϕ, let ϕ M denote the set of all the states of M that satisfies ϕ.
The semantics of ATL/ATL * defined on ACGS is different from the one defined on CGS, hence they are incomparable.
Proposition 1 There are an ACGS M = (G, π), an ATL/ATL * formula A φ, and a type σ ∈ T str such that π(i) = σ for all i ∈ A and M, s | = A φ holds, but G, s | = σ A φ.

Model-Checking Algorithms
It has been shown that the Turing Halting problem can be reduced to the model-checking problem of CGS against the ATL formula ϕ = {1, 2} G ok under the iR setting [Dima and Tiplea, 2011], where ok is an atomic proposition. By adapting the proof, we get that: By Theorem 1, we focus on the model-checking problem of ACGS by restricting the function π to Ag → T str \ {iR}. In general, we propose model-checking algorithms which iteratively compute the set of states satisfying state formulae from the innermost subformulae. The main challenge is to compute A φ M . To this end, we first show how to compute A φ M for a simple formula A φ, and then present the more general algorithm. An ATL/ATL * formula A φ is called simple if φ is an LTL formula.
Let us fix an ACGS M = (G, π) with G = (S , S 0 , Ag, (Ac i ) i∈Ag , (∼ i ) i∈Ag , (P i ) i∈Ag , ∆, λ) and a simple formula A φ. Given a set of agents A ′ and a strategy type σ ∈ T str , we denote by A ′ σ the set {i ∈ A ′ | π(i) = σ}.

Model-Checking Simple ATL Formulae
For a simple ATL formula A φ, it is easy to see that whether agents in A have perfect call or not does not matter if these agents have perfect information abilities.
Proposition 2 Given an ACGS (G, π) with π : Ag → T str \ {iR}, and a simple ATL formula A ϕ, let π ′ be a function such that for By Proposition 2, all the agents in A with IR-strategies can be seen as agents with Ir-strategies. All the agents in Ag with Ir-strategies can be seen as agents with ir-strategies (i.e., all the epistemic accessibility relations of them are the identity relation). Therefore, we can assume that π(i) = ir for all i ∈ A, and π(i) ∈ {ir, IR} for all i ∈ A. For two collective strategies ξ A and ξ A ir , let M(ξ A , ξ A ir ) = (G ′ , π) be the ACGS obtained from (G, π) by enforcing strategies ξ A and ξ A ir , namely, by removing transitions whose actions of agents in A ∪ A ir do not conform to ξ A and ξ A ir . We have that Computing ∅ φ M(ξ A ,ξ A ir ) amounts to CTL modelchecking, which can be done in polynomial time (and thus et al., 1983]. Since the number of strategies ξ A and ξ A ir is finite, we get that:

Model-Checking Simple ATL * Formulae
We compute A φ M by a reduction to the problem of computing the winning region of a turn-based two-player parity game. We first introduce some basic concepts which will be used in our reduction.
Let inf(ρ) be the set of states visited infinitely often in ρ. An infinite word is recognized by A if A has a run ρ over this word such that min p∈inf(ρ) R(p) is even. For the LTL formula φ, one can construct a DPA A φ = (P, 2 AP , δ, p 0 , R) with 2 2 O(|φ|) states and rank k = 2 O(|φ|) such that A φ recognizes all the ω-words satisfying φ [Piterman, 2006].
A (turned-based, two-player) parity game P is a tuple ( Given a strategy θ 0 for Player-0 and a strategy θ 1 for Player-1, let G θ 0 ,θ 1 be the play where Player-0 and Player-1 enforce their strategies θ 0 and θ 1 . θ 0 is a winning strategy for Player-0 if min s∈inf(G θ 0 ,θ 1 ) Ξ(s) is even for every strategy θ 1 of Player-1. The winning region of Player-0, denoted by WR 0 , is the set of vertices from which Player-0 has a winning strategy.
A partial strategy of A ′ is a partial function f : and g ⊥ ∈ G ir denote the partial strategy such that dom(g ⊥ ) = ∅. Given a state s, let F s IR be the set of functions f : A IR → i∈A IR Ac i such that for every i ∈ A IR , f (i) ∈ P i (s). Let F IR := s∈S F s IR and Π ir : We define a parity game k} is a function such that for every s ∈ S , ir , ∀ f ∈ F IR and ∀G ∈ Π ir , E is defined as follows: where G ′ ⊆ Π ir is the largest set such that the follows hold: for every g ′ ∈ G ′ , In this reduction, f ⊤ encodes a collective ir-strategy of agents in A ir , the collection of f 's in one play of P φ encodes a collective IR-strategy of agents in A IR , and each g ∈ G encodes a collective ir-strategy of agents in A ir . The imperfect information abilities of agents are ensured by the definitions partial strategies.
To check whether s ∈ A φ M , P φ starts with the vertex s. At first step, Player-0 chooses a function f ⊤ ∈ F ⊤ ir meaning that all agents in A ir choose an ir-strategy. Next, P φ moves from (s, f ⊤ ) to (s, p 0 , f ⊤ , {g ⊥ }) which let the DPA A φ start with p 0 (note that Player-1 has only one choice at this step). At a vertex (s, p, f ⊤ , G) controlled by Player-0, Player-0 chooses actions for agents in A IR by choosing one function f ∈ F s IR . Then Player-1 chooses actions for agents in A with respect to the chosen actions of agents in A ir tracked by G. These selections of actions together with f ⊤ and G determine a joint action a, based on which P φ moves to (s ′ , δ(p, λ(s)), f ⊤ , G ′ ) such that s ′ is the next state of s under a, δ(p, λ(s)) is the next state of p in A φ which allows to mimics the run of A φ over the ω-word induced by the play of M. During this step, f is dropped from the vertex of P φ , as f corresponds to actions of agents in A IR and needs not to track. The actions of agents in A ir are tracked by computing G ′ from G. This ensures imperfect recall abilities of agents in A ir . We then can get that: The winning region of Player-0 in P φ can be computed in polynomial time of |V| · |E| · 2 k [Jurdzinski, 2000]. In this reduction, each G contributes at most O(|S |) sets of G ′ . Therefore, |V| · |E| is exponential in |G| · 2 |φ| . Recall that k = 2 O(|φ|) .

Lemma 3 For the simple ATL * formula A φ,
A φ M can be computed in 2EXPTIME.

12
Compute A φ M by Lemma 1 or 3; 13 return A φ M ;

The Overall Algorithm
We now present the overall procedure, which computes ϕ M from the innermost subformulae. Algorithm 1 shows the pseudo code, which takes an ACGS M = (G, π) and an ATL/ATL * formula ϕ as inputs, and outputs ϕ M . Then M satisfies ϕ iff the set of initial states of M is a subset of ϕ M . We also incorporate epistemic modalities Hoek and Wooldridge, 2003;Cermák et al., 2014] into our algorithm with the following semantics: . K i ϕ, E A ϕ, D A ϕ and C A ϕ respectively denote that i knows, every agent in A knows, agents in A have common knowledge and agents in A have distributed knowledge, on the fact ϕ. The ATL (resp. ATL * ) logic extended with these epistemic modalities is called ATLK (resp. ATLK * ) logic. Given a state s ∈ S and a binary relation ⋍⊆ S × S , we denote by [s] ⋍ the set {s ′ ∈ S | s ⋍ s ′ }.
By Lemma 1 and Lemma 3, the model-checking problem for ATLK and ATLK * on ACGS can be solved in PSPACE and 2EXPTIME respectively. As the model-checking problem of ATL * on CGS under IR setting is 2EXPTIMEcomplete [Alur et al., 2002], we have that Theorem 2 The model-checking problem for ATLK * (resp. ATLK) on ACGS is 2EXPTIME-complete (resp. in PSPACE).  In this CG game, there are several agents modelling workers and an environment agent. Each worker works for the benefit of a castle, and the environment keeps track of the Health Points (HP) of castles. Each castle preserves an HP valued up to 3, and 0 means it's defeated. Workers are able to attack a castle which they don't work for, or defend the castle which they work for, or do nothing. The castle gets damaged if the number of attackers is greater than the number of defenders, and the differences influence its HP. In this model, the number of states is 8000 × 4n, the environment agent has 1 local action, and each worker agent has 4 local actions, where n denotes the number of workers.

Implementation and Experiments
In this experiment, we consider ACGS consisting of three worker agents w 1 , w 2 , w 3 and an environment agent e, where worker w i works for the castle c i .
• ϕ 1 ≡ {w 1 , w 2 } F(castle3De f eated): expresses that workers w 1 and w 2 can make castle c 3 defeated, no matter which strategies other agents use.
• ϕ 2 ≡ {w 1 , w 2 } F(allDe f eated): expresses that workers w 1 and w 2 can make all the castles defeated, no matter which strategies other agents use.
We observe that: (1) the strategy types of agents do affect the performance and results. In particular, the time significantly increases when w 3 is ir-typed while w 1 or w 2 is IRtyped; (2) Lemma 1 is more efficient when both w 1 and w 2 are ir-typed; otherwise Lemma 3 is more efficient. This is because the number of possible strategies of w 1 and w 2 is small (using Lemma 1) if both w 1 and w 2 are ir-typed.

Related Work
The family of alternating-time temporal logics ATL, ATL * and alternating µ-calculus (AMC) [Alur et al., 2002] for rea-soning about games was introduced with motivations partially from MAS. Model-checking algorithms were also given with IR-strategies. [van der Hoek and Wooldridge, 2003] extended ATL with knowledge operators and proposed corresponding model-checking algorithms. In their work, epistemic accessibility relations are considered in the interpretation of knowledge operators, but not for the strategies and outcomes. This means that agents still use IR strategies for coalition modalities A ψ. This issue was discussed in [Jamroga, 2003] which proposed an idea of iRstrategies. [Schobbens, 2004] introduced the notion of imperfect recall into ATL/ATL * , and investigated the modelchecking problem for ATL/ATL * under four different strategic types. Importantly, with iR-strategies the model-checking problem becomes undecidable [Dima and Tiplea, 2011].
[Bulling and Jamroga, 2011] studied the semantics of AMC and proposed a model-checking algorithm for the alternationfree fragment under the imperfect information setting.
[Bulling and Jamroga, 2014] further conducted a comprehensive comparison of variants of ATL/ATL * with different strategic types. The study corroborate that the agents' abilities play a prominent role in logic semantics.
In the previous work, strategies are revocable, i.e., when it comes to achieve a goal in the (nested) sub-formula, previously selected strategies are deleted. [Ågotnes et al., 2007] introduced a variant of ATL with irrevocable strategies under the imperfect recall setting. It was generalized into ATL/ATL * with strategy contexts [Laroussinie and Markey, 2015], which allows agents to drop or inherit previously selected strategies.
Two strategic logics were introduced by [Chatterjee et al., 2010] and [Mogavero et al., 2014] and the model-checking problem was investigated therein under the IR-setting. Strategic logics extend LTL with first-order quantifications over strategies which naturally captures the multi-player game nature in the evolution of MAS. [Cermák et al., 2014] introduced knowledge operators in the strategic logic of [Mogavero et al., 2014] and proposed a model-checking algorithm with ir-strategies. Here all agents must take ir-strategies (so the potential inconsistency can be ruled out), but no other abilities are considered. To gain decidability under iR-setting, specific restrictions on the abilities of the agents were proposed [Berthon et al., 2017a;Berthon et al., 2017b;Belardinelli et al., 2017a;Belardinelli et al., 2018].
Our work is orthogonal to the existing work which defines the agents' abilities at the semantics level, but takes a more syntactic level by strengthening the model.

Conclusion and Future Work
In this paper, we discussed the problem of existing semantics of ATL/ATL * , and advocated the approach to make agents' abilities explicit in modeling. For this purpose, we introduced an extension of standard CGS model, i.e. ACGS, which define agents' abilities at the syntactic level of the system model. We explored the effects of strategy types in the semantics, in particular model-checking, of ATL/ ATL * over ACGS, and pro-vided model-checking algorithms with identified complexity. The algorithms are implemented in a tool MCMAS-ACGS, which has been applied to several applications to demonstrate the feasibility of the approach. This work represents the first systematic study towards different agents' abilities at the syntactic level, which is in contrast to the previous approaches at the semantic level.
Currently we use ATL/ATL * as the specification, but the methodology can be extended to other logics such as Strategy Logic, and other agents' abilities such as strategy contexts. Several questions are left open such as axiomatization and satisfiability problem. We leave them for future work.

A Proof of Theorem 1
Given a Turing machine M, let G = (S , {s 0 }, Ag, (Ac i ) i∈Ag , (∼ i ) i∈Ag , (P i ) i∈Ag , ∆, λ) be the CGS constructed as in [Dima and Tiplea, 2011] and s 0 be an initial state in G such that G, s 0 | = iR {1, 2} G ok iff M does not halt on the empty word. Let M = (G, π) be an ACGS such that for every agent i in M, π(i) = iR if i ∈ {1, 2}, otherwise π(i) = IR. Therefore, The result immediately follows.

B Proof of Proposition 2
Without loss of generality, we assume that for every i ∈ Ag, π(i) Ir, as Ir can be seen as a special case of ir. We first construct the tree-unfolding of M from the state s.
(⇐) Suppose M * s , s | = A ϕ, let ξ * A be the collective strategy such that for every path ρ ∈ O M * s (s, ξ * A ), M * s , ρ | = ϕ. We assume that there is a total order on set S + , and denote by min(U) the minimal one of the set of states U ⊆ S + with respect to the order . Let ξ A be the function such that for every i ∈ A and s ′ ∈ S , ξ A (i)(s ′ ) = ξ * A (i)(min({ρ ∈ S + | lst(ρ) = s ′ })). First, we show that ξ A is a collective strategy of A in M ′ . Consider an agent i ∈ A and two states s 1 , s 2 ∈ S such that s 1 ∼ i s 2 , if π(i) IR, then for each pair of states ρ 1 , ρ 2 ∈ S + such that lst(ρ 1 ) = s 1 and lst(ρ 2 ) = s 2 , we have ρ 1 ∼ * i ρ 2 , which implies that ξ * . The result immediately follows from the fact that λ * (ρ) = λ(lst(ρ)) for every ρ ∈ S + .
⊓ ⊔ Recalling that [Alur et al., 2002] observed that both semantics of ATL under Ir-strategies and IR-strategies coincide for CGS . This result was generalized and formally proved in infinite CGS (i.e., no finiteness with respect to the set of states and actions) (cf. Proposition 1 [Bulling and Jamroga, 2014]). Proposition 2 can be seen as a generalization of the result of [Alur et al., 2002] and could be extended to the infinite ACGS similar to [Bulling and Jamroga, 2014].

C Effects of Strategy Types
By restricting all the strategy types to IR, straightforwardly we have: Proposition 3 Let M = (G, π) be an ACGS where for each i ∈ Ag, π(i) = IR. For each state s of M and ATL * formula ϕ, G, s | = IR ϕ iff M, s | = ϕ.
Proof. By applying structural induction, it suffices to show that the result holds for formulae of the form A φ. By applying induction hypothesis, for every path ρ, the following holds: . Each i ∈ A has same sets of possible IR-strategies in G and M, hence ⊓ ⊔ In light of Proposition 1 and Proposition 3, we shall investigate the effects of strategy types by considering ACGS with various different setups of strategy types.
Lemma 4 Let A be a set of agents and s be a state of a CGS G. For two functions π 1 , π 2 : Ag → T str with π 1 A π 2 , and any collective strategy ξ A of A, we have: Lemma 4 reveals the effect of strategy types of A on the outcomes. It is easy to observe that if π 2 (i) = σ for all i ∈ A, then for every collective σ-strategy υ σ (3) negations ¬ only appear in front of atomic propositions. For example, A X q is positive, while ¬ A X q is not positive. Given a formula ϕ, let Ag ϕ denote the set of agents that appear in ϕ. By Lemma 4, we have: Proposition 4 Let G be a CGS, s be a state of G and ϕ be a positive ATL/ATL * formula. For π 1 , π 2 : Ag → T str such that π 1 Ag ϕ π 2 , if (G, π 2 ), s | = ϕ, then (G, π 1 ), s | = ϕ.
Proof. By applying structural induction, it suffices to show that the result holds for formulae of the form A φ. We suppose (G, π 2 ), s | = A φ, otherwise Item 1 immediately holds.
⊓ ⊔ For positive ATL/ATL * formulae ϕ, even if the agents of Ag ϕ have the same strategy types in ACGS (G, π) and CGS G, verifying G against ϕ under σ will examine more behavior than verifying (G, π) against ϕ, where i ∈ Ag ϕ and π(i) = σ. Therefore, if the behavior of a MAS is exactly modeled as an ACGS M rather than a CGS G with strategy type σ, verifying G against ϕ under σ may lead to incorrect result. However, more restrictions on strategy types and ATL/ATL * formulae can make them coincide, as the following proposition shows.

D.1 Experiment on Dining Cryptographers Protocol
Dining cryptographers protocol is one of anonymity protocols aimed at establishing the privacy of principals during an exchange . The dining cryptographers protocol can be modeled as MAS. In this game, n cryptographers share a meal around a circular table. Either one of them or their employer paid for the meal. They are curious whether it was sponsored by their employer without revealing the identity of the payer (if one of them did pay). The protocol works as follows: each cryptographer 1) tosses a coin and shows the outcome to his right-hand neighbour, 2) announces whether the two coins agree or not if he/she is not payer, otherwise announces the opposite of what he/she sees. Their employer is the payer if an even number of cryptographers claiming that the two coins are different, otherwise not. For experimental purpose, we allow the cryptographer who paid for the meal announces either the two coins agree or not no matter what he/she saw.
In this experiment, n ranges from 3 to 10, a cryptographer whose is payer and one of other cryptographers use ir-strategies, the others all use IR-strategies. We verify three formulae ψ 1 , ψ 2 and ψ 3 , where ψ i expresses that if the number of "saydifferent"  is odd and the i-th cryptographer is not the payer, then he/she knows that the bill is paid by one of the others, but cannot tell exactly who is the payer. For instance, in the three cryptographers case, The results are shown in Table 2, where column 1 gives the number of cryptographers, column 2 gives the number of states, columns 3-5 (resp. columns 6-7) show the total time of respectively verifying ψ 1 , ψ 2 and ψ 3 using Lemma 1 (resp. Lemma 3). Both ψ 1 and ψ 2 are satisfied by all the models, while ψ 3 not. We observe that Lemma 1 is more efficient than Lemma 3, as the coalitions in all the formulae are ∅. From this experiment, one may conclude the reasonable scalability of our tool.

D.2 Experiment on Book Store Scenario (BSS)
The BSS model depicts a deal between two agents: a supplier (S) and a purchaser (P) . Initially, S is waiting for an order from P, and P is ready for initiating a trade. Upon receiving an order of some e-good from P, S can make a decision whether accepts the order or not do, and later notify P. If S accepts, then P can pay fee. Once paid, S can either reject the payment or accept and deliver the good. If P received the good, then trade is completed. During the trade, P can revoke the order, both S and P can terminate the trade, after which the information of the trade should be symmetric at any time. In this model, the S has 15 local states and 13 actions, and P has 12 local states and 7 actions. In this experiment, we verify the model against the following formulae. ϕ 1 ≡ ∅ G((S &P no T ) → (K S {S , P} F trade end)) expresses that "if neither S nor P terminates the trade (i.e., S &P no T is ture), then S knows that they can cooperatively complete the trade eventually" always holds. ϕ 2 ≡ {S , P} (S &P no T U(trade end ∧ ¬trade success)) expresses that the trade can ends by P asking for refund.
The results are shown in Table 3. Each row presents the result of one of strategy type combinations of S and P, for instance, (IR, ir) denotes that S has an IR-strategy while P has ir-strategy. Columns 2-4 (resp. columns 5-7) show total time and result of verifying ϕ 1 (resp. ϕ 2 ) using Lemma 1 (resp. Lemma 3). The results of ϕ 1 confirm that strategy types affect the truth of formulae. Lemma 1 performs better than Lemma 3 both on ϕ 1 and ϕ 2 in this experiment.