François Laroussinie

Nicolas Markey

Ghassan Oreiby

On the Expressiveness and Complexity of ATL

ATL is a temporal logic geared towards the specification and verification of properties in multi-agents systems. It allows to reason on the existence of strategies for coalitions of agents in order to enforce a given property. We prove that the standard definition of ATL (built on modalities "Next", "Always" and "Until") has to be completed in order to express the duals of its modalities: it is necessary to add the modality "Release". We then precisely characterize the complexity of ATL modelchecking when the number of agents is not fixed. We prove that it is ∆ P 2and ∆ P 3 -complete, depending on the underlying multi-agent model (ATS and CGS resp.). We also prove that ATL + model-checking is ∆ P 3 -complete over both models, even with a fixed number of agents.

Introduction

Model checking. Temporal logics were proposed for the specification of reactive systems almost thirty years ago [START_REF] Pnueli | The temporal logic of programs[END_REF]. They have been widely studied and successfully used in many situations, especially for model checking -the automatic verification that a finite-state model of a system satisfies a temporal logic specification. Two flavors of temporal logics have mainly been studied: linear-time temporal logics, e.g. LTL [START_REF] Pnueli | The temporal logic of programs[END_REF], which expresses properties on the possible executions of the model; and branching-time temporal logics, such as CTL [START_REF] Clarke | Design and synthesis of synchronous skeletons using branching-time temporal logic[END_REF][START_REF] Queille | Specification and verification of concurrent systems in CESAR[END_REF], which can express requirements on states (which may have several possible futures) of the model.

Alternating-time temporal logic. Over the last ten years, a new flavor of temporal logics has been defined: alternating-time temporal logics, e.g. ATL [START_REF] Alur | Alternating-time temporal logic[END_REF][START_REF] Alur | Alternating-time temporal logic[END_REF]. ATL is a fundamental logic for verifying properties in synchronous multi-agent systems, in which several agents can concurrently influence the behavior of the system. This is particularly interesting for modeling control problems. In that setting, it is not only interesting to know if something can arrive or will arrive, as can be expressed in CTL or LTL, but rather if some agent(s) can control the evolution of the system in order to enforce a given property.

The logic ATL can precisely express this kind of properties, and can for instance state that "there is a strategy for a coalition A of agents in order to eventually reach an accepting state, whatever the other agents do". ATL is an extension of CTL, its formulae are built on atomic propositions and boolean combinators, and (following the seminal papers [START_REF] Alur | Alternating-time temporal logic[END_REF][START_REF] Alur | Alternating-time temporal logic[END_REF]) on modalities A X ϕ (coalition A has a strategy to immediately enter a state satisfying ϕ), A G ϕ (coalition A can force the system to always satisfy ϕ) and A ϕ U ψ (coalition A has a strategy to enforce ϕ U ψ).

Multi-agent models. While linear-and branching-time temporal logics are interpreted on Kripke structure, alternating-time temporal logics are interpreted on models that incorporate the notion of multiple agents. Two kinds of synchronous multi-agent models have been proposed for ATL in the literature. First Alternating Transition Systems (ATSs) [START_REF] Alur | Alternating-time temporal logic[END_REF] have been defined: in any location of an ATS, each agent chooses one move, i.e., a subset of locations (the list of possible moves is defined explicitly in the model) in which he would like the execution to go to. When all the agents have made their choice, the intersection of their choices is required to contain one single location, in which the execution enters. In the second family of models, called Concurrent Game Structures (CGSs) [START_REF] Alur | Alternating-time temporal logic[END_REF], each of the n agents has a finite number of possible moves (numbered with integers), and, in each location, an n-ary transition function indicates the state to which the execution goes.

Our contributions. While in LTL and CTL, the dual of "Until" modality can be expressed as a disjunction of "always" and "until", we prove that it is not the case in ATL. In other words, ATL, as defined in [START_REF] Alur | Alternating-time temporal logic[END_REF][START_REF] Alur | Alternating-time temporal logic[END_REF], is not as expressive as one could expect (while it is known that adding the dual of "Until" does not increase the complexity of the verification problems [START_REF] Alur | Mocha: Modularity in model checking[END_REF][START_REF] Goranko | Complete axiomatization and decidability of alternating-time temporal logic[END_REF]).

We also precisely characterize the complexity of the model checking problem. The original works about ATL provide model-checking algorithms in time O(m • l), where m is the number of transitions in the model, and l is the size of the formula [START_REF] Alur | Alternating-time temporal logic[END_REF][START_REF] Alur | Alternating-time temporal logic[END_REF], thus in PTIME. However, contrary to Kripke structures, the number of transitions in a CGS or in an ATS is not quadratic in the number of states [START_REF] Alur | Alternating-time temporal logic[END_REF], and might even be exponential in the number of agents. PTIMEcompleteness thus only holds for ATS when the number of agents is bounded, and it is shown in [START_REF] Jamroga | Do agents make model checking explode (computationally)?[END_REF][START_REF] Jamroga | Model checking abilities of agents: A closer look[END_REF] that the problem is strictly1 harder otherwise, namely NP-hard on ATS and Σ P 2 -hard on CGSs where the transition function is encoded as a boolean function. We prove that it is in fact ∆ P 2 -complete and ∆ P 3 -complete, resp., correcting wrong algorithms in [START_REF] Jamroga | Do agents make model checking explode (computationally)?[END_REF][START_REF] Jamroga | Model checking abilities of agents: A closer look[END_REF] (the problem lies in the way the algorithms handle negations). We also show that ATL + is ∆ P 3 -complete on both ATSs and CGSs, even when the number of agents is fixed, extending a result of [START_REF] Schobbens | Alternating-time logic with imperfect recall[END_REF]. Finally we study translations between ATS and CGS. Related works. In [START_REF] Alur | Alternating-time temporal logic[END_REF][START_REF] Alur | Alternating-time temporal logic[END_REF] ATL has been proposed and defined over ATS and CGS. In [START_REF] Harding | Approximating ATL * in ATL[END_REF] expressiveness issues are considered for ATL * and ATL. Complexity of satisfiability is addressed in [START_REF] Goranko | Complete axiomatization and decidability of alternating-time temporal logic[END_REF][START_REF] Walther | ATL satisfiability is indeed EXPTIME-complete[END_REF]. Complexity results about model checking (for ATL, ATL + , ATL * ) can be found in [START_REF] Alur | Alternating-time temporal logic[END_REF][START_REF] Schobbens | Alternating-time logic with imperfect recall[END_REF]. Regarding control-and game theory, many papers have focused on this wide area; we refer to [START_REF] Walukiewicz | A landscape with games in the background[END_REF] for a survey, and to its numerous references for a complete overview.

Plan of the paper. Section 2 contains the necessary formal definitions needed in the sequel. Section 3 explains our expressiveness result, and Section 4 deals with the model-checking algorithms. Due to lack of space, some proofs are omitted in this article, but can be read in the technical appendix at the end of the paper. The intended behaviour is as follows [START_REF] Alur | Alternating-time temporal logic[END_REF]: in a given location , each player A i chooses one possible move m Ai in Mov( , A i ) and the successor location is given by Edg( , m A1 , ..., m A k ). We write Next( ) for the set of all possible successor locations from , and Next( , A j , m) for the restriction of Next( ) to locations reachable from when player A j makes the move m.

Definitions

In the original works about ATL [START_REF] Alur | Alternating-time temporal logic[END_REF], the logic was interpreted on ATSs, which are transition systems slightly different from CGSs: Definition 2. An Alternating Transition System ( ATS for short) A is a 5-tuple (Agt, Loc, AP, Lab, Mov) where:

-Agt, Loc, AP and Lab have the same meaning as in CGSs; -Mov : Loc×Agt → P(P(Loc)) associate with each location and each agent a the set of possible moves, each move being a subset of Loc. For each location , it is required that, for any

Q i ∈ Mov( , A i ), i≤k Q i be a singleton.
The intuition is as follows: in a location , once all the agents have chosen their moves (i.e., a subset of locations), the execution goes to the (only) state that belongs to all the sets chosen by the players. Again Next( ) (resp. Next( , A j , m)) denotes the set of all possible successor locations (resp. the set of possible successor locations when player A j chooses the move m).

We prove in Section 4.2 that both models have the same expressiveness (w.r.t. alternating bisimilarity [START_REF] Alur | Alternating refinement relations[END_REF]).

Strategy, outcomes of a strategy

Let S be a CGS or an ATS. A computation of S is an infinite sequence ρ = 0 1 • • • of locations such that for any i, i+1 ∈ Next( i ). We can use the standard notions of suffix and prefix for these computations; ρ[i] denotes the i-th location i . A strategy for a player A i ∈ Agt is a function f Ai that maps any finite prefix of a computation to a possible move for A i2 . A strategy is state-based (or memoryless) if it only depends on the current state (i.e., f Ai ( 0

• • • m ) = f Ai ( m )).
A strategy induces a set of computations from -called the outcomes of f Ai from and denoted 3 Out S ( , f Ai )-that player A i can enforce:

0 1 2 • • • ∈ Out S ( , f Ai ) iff = 0 and for any i we have i+1 ∈ Next( i , A i , f Ai ( 0 • • • i )).
Let A ⊆ Agt be a coalition. A strategy for A is a tuple F A containing one strategy for every player in A: F A = {f Ai |A i ∈ A}. The outcomes of F A from a location contains the computations enforced by the strategies in

F A : 0 1 • • • ∈ Out S ( , F A ) s.t. = 0 and for any i, i+1 ∈ Ai∈A Next( i , A i , f Ai ( 0 • • • i )).
The set of strategies for A is denoted 3 Strat S (A). Finally Out S ( , ∅) represents the set of all computations from .

The logic ATL and some extensions

Again, we follow the definitions of [START_REF] Alur | Alternating-time temporal logic[END_REF]: Definition 3. The syntax of ATL is defined by the following grammar:

ATL ϕ s , ψ s ::= | p | ¬ϕ s | ϕ s ∨ ψ s | A ϕ p ϕ p ::= X ϕ s | G ϕ s | ϕ s U ψ s .
where p ranges over the set AP and A over the subsets of Agt.

In addition, we use standard abbreviations like , ⊥, F , etc. ATL formulae are interpreted over states of a game structure S. The semantics of the main modalities is defined as follows 3 :

|= S A ϕ p iff ∃F A ∈ Strat(A). ∀ρ ∈ Out( , F A ). ρ |= S ϕ p , ρ |= S X ϕ s iff ρ[1] |= S ϕ s , ρ |= S G ϕ s iff ∀i. ρ[i] |= S ϕ s , ρ |= S ϕ s U ψ s iff ∃i. ρ[i] |= S ψ s and ∀0 ≤ j < i. ρ[j] |= S ϕ s .
It is well-known that, for the logic ATL, it is sufficient to restrict to state-based strategies (i.e., A ϕ p is satisfied iff there is a state-based strategy all of whose outcomes satisfy ϕ p ) [START_REF] Alur | Alternating-time temporal logic[END_REF][START_REF] Schobbens | Alternating-time logic with imperfect recall[END_REF]. Note that ∅ ϕ p corresponds to the CTL formula Aϕ p (i.e., universal quantification over all computations issued from the current state), while Agt ϕ p corresponds to existential quantification Eϕ p . Note, however, that ¬ A ϕ p is generally not equivalent to Agt A ¬ϕ p [START_REF] Alur | Alternating-time temporal logic[END_REF][START_REF] Goranko | Complete axiomatization and decidability of alternating-time temporal logic[END_REF]. Fig. 1 displays a (graphical representation of a) 2-player CGS for which, in 0 , both ¬ A 1 X p and ¬ A 2 ¬X p hold. In such a representation, a transition is labeled with m 1 .m 2 when it correspond to move m 1 of player A 1 and to move m 2 of player A 2 . Fig. 2 represents an (alternating-bisimilar) ATS with the same properties.

0 p 1 ¬p 1 ¬p 2 p 2 1.1 1.2 2.1 2.2
Fig. 1. A CGS that is not determined.

Loc = { 0, 1, 2, 1 , 2 } Mov( 0, A1) = {{ 1, 1 }, { 2, 2 }} Mov( 0, A2) = {{ 1, 2 }, { 2, 1 }} with ( Lab( 1) = Lab( 2) = {p} Lab( 1 ) = Lab( 2 ) = ∅ Fig. 2. An ATS that is not determined.
Duality is a fundamental concept in modal and temporal logics: for instance, the dual of modality U, often denoted by R and read release, is defined by

ϕ s R ψ s def ≡ ¬((¬ϕ s ) U (¬ψ s )).
Dual modalities allow, for instance, to put negations inner inside the formula, which is often an important property when manipulating formulas. In LTL, modality R can be expressed using only U and G:

ϕ R ψ ≡ G ψ ∨ ψ U (ϕ ∧ ψ). (1)
In the same way, it is well known that CTL can be defined using only modalities EX, EG and EU, and that we have

Eϕ R ψ ≡ EG ψ ∨ Eψ U (ϕ ∧ ψ) Aϕ R ψ ≡ ¬ E(¬ϕ) U (¬ψ).
We prove in the sequel that modality R cannot be expressed in ATL, as defined in Definition 3. We thus define the following two extensions of ATL: Definition 4. We define ATL R and ATL + with the following syntax:

ATL R ϕ s , ψ s ::= | p | ¬ϕ s | ϕ s ∨ ψ s | A ϕ p ϕ p ::= X ϕ s | ϕ s U ψ s | ϕ s R ψ s , ATL + ϕ s , ψ s ::= | p | ¬ϕ s | ϕ s ∨ ψ s | A ϕ p ϕ p , ψ p ::= ¬ϕ p | ϕ p ∨ ψ p | X ϕ s | ϕ s U ψ s | ϕ s R ψ s .
where p ranges over the set AP and A over the subsets of Agt.

Given a formula ϕ in one of the logics we have defined, the size of ϕ, denoted by |ϕ|, is the size of the tree representing that formula. The DAG-size of ϕ is the size of the directed acyclic graph representing that formula (i.e., sharing common subformulas).

A (a R b) cannot be expressed in ATL

This section is devoted to the expressiveness of ATL. We prove:

Theorem 5. There is no ATL formula equivalent to Φ = A (a R b).
The proof of Theorem 5 is based on techniques similar to those used for proving expressiveness results for temporal logics like CTL or ECTL [START_REF] Emerson | Temporal and modal logic[END_REF]: we build two families of models (s i ) i∈N and (s i ) i∈N s.t. (1) s i |= Φ, (2) s i |= Φ for any i, and (3) s i and s i satisfy the same ATL formula of size less than i. Theorem 5 is a direct consequence of the existence of such families of models. In order to simplify the presentation, the theorem is proved for formula 4

Φ = A (b R (a ∨ b)).
The models are described by one single inductive CGS5 C, involving two players. It is depicted on Fig. 3. A label α.β on a transition indicates that this

a a i a s i-1 a a i-1 a s 1 a a 1 b b i b b 1 a si a s i a s i-1 a s 1 ¬a, ¬b s 0 3.1 3.1 3.1 3.1 , 4.2 3.1 , 4.2 3.1 , 4.2 2.2 2.3 2.2 2.3 2.2 2.3 2.2 2.3 4.3 2.2 2.3 4.3 2.2 2.3 4.3 1.1 1.1 1 . 1 4 . 1 1 . 1 4 . 1 1.2 , 1.3 2.1 , 3.2 , 3.3 1.2 , 1.3 2.1 , 3.2 , 3.3 1 . 2 , 1 . 3 , 2 . 1 , 3 . 2 , 3 . 3 1 . 2 , 1 . 3 , 2 . 1 , 3 . 2 , 3 . 3
Fig. 3. The CGS C, with states si and s i on the left transition corresponds to move α of player A 1 and to move β of player A 2 . In that CGS, states s i and s i only differ in that player A 1 has a fourth possible move in s i . This ensures that, from state s i (for any i), player A 1 has a strategy (namely, he should always play 4) for enforcing a W b. But this is not the case from state s i : by induction on i, one can prove s i |= A 1 a W b. The base case is trivial. Now assume the property holds for i: from s i+1 , any strategy for A 1 starts with a move in {1, 2, 3} and for any of these choices, player A 2 can choose a move (2, 1 and 2 resp.) that enforce the next state to be s i where by i.h. A 1 has no strategy for a W b.

We now prove that s i and s i satisfy the same "small" formulae. First, we have the following equivalences: Lemma 6. For any i > 0, for any ψ ∈ ATL with |ψ| ≤ i:

b i |= ψ iff b i+1 |= ψ s i |= ψ iff s i+1 |= ψ s i |= ψ iff s i+1 |= ψ
The proof may be found in Appendix A.

Lemma 7. ∀i > 0, ∀ψ ∈ ATL with |ψ| ≤ i: s i |= ψ iff s i |= ψ.
Proof. The proof proceeds by induction on i, and on the structure of the formula ψ. The case i = 1 is trivial, since s 1 and s 1 carry the same atomic propositions. For the induction step, dealing with CTL modalities ( ∅ and A 1 , A 2 ) is also straightforward, then we just consider A 1 -and A 2 modalities. First we consider A 1 -modalities. It is well-known that we can restrict to state-based strategies in this setting. If player A 1 has a strategy in s i to enforce something, then he can follow the same strategy from s i . Conversely, if player A 1 has a strategy in s i to enforce some property, two cases may arise: either the strategy consists in playing move 1, 2 or 3, and it can be mimicked from s i . Or the strategy consists in playing move 4 and we distinguish three cases:

ψ = A 1 X ψ 1 : that move 4 is a winning strategy entails that s i , a i and b i must satisfy ψ 1 . Then s i (by i.h. on the formula) and s i-1 (by Lemma 6) both satisfy ψ 1 . Playing move 1 (or 3) in s i ensures that the next state will satisfy ψ 1 .

-ψ = A 1 G ψ 1 : by playing move 4, the game could end up in s i-1 (via b i ),
and in a i and s i . Thus s i-1 |= ψ, and in particular ψ 1 . By i.h., s i |= ψ 1 , and playing move 1 (or 3) in s i , and then mimicking the original strategy (from s i ), enforces G ψ 1 . ψ = A 1 ψ 1 U ψ 2 : a strategy starting with move 4 implies s i |= ψ 2 (the game could stay in s i for ever). Then s i |= ψ 2 by i.h., and the result follows.

We now turn to A 2 -modalities: clearly if A 2 ψ 1 holds in s i , it also holds in s i . Conversely, if player A 2 has a (state-based) strategy to enforce some property in s i : If it consists in playing moves 1 or 3, then the same strategy also works in s i . Now if the strategy starts with move 2, then playing move 3 in s i has the same effect, and thus enforces the same property.

Remark 1. ATL and ATL R have the same distinguishing power as the fragment of ATL involving only the • X modality (see [START_REF] Alur | Alternating refinement relations[END_REF]proof of Th. 6]). This means that we cannot exhibit two models M and M s. Even if ATL + would not contain the "release" modality in its syntax, it can express it, and it is thus strictly more expressive than ATL. However, as for CTL and CTL + , it is possible to translate ATL + into ATL R [START_REF] Harding | Approximating ATL * in ATL[END_REF]. Of course, such a translation induces at least an exponential blow-up in the size of the formulae since it is already the case when translating CTL + into CTL [START_REF] Th | CTL + is exponentially more succinct than CTL[END_REF][START_REF] Adler | An n! lower bound on formula size[END_REF]. Finally note that the standard model-checking algorithm for ATL easily extends to ATL R (and that Mocha [START_REF] Alur | Mocha: Modularity in model checking[END_REF] handles ATL R formulae). In the same way, the axiomatization and satisfiability results of [START_REF] Goranko | Complete axiomatization and decidability of alternating-time temporal logic[END_REF] can be extended to ATL R (as mentioned in the conclusion of [START_REF] Goranko | Complete axiomatization and decidability of alternating-time temporal logic[END_REF]).

Turn-based games. In [START_REF] Alur | Alternating-time temporal logic[END_REF], a restriction of CGS -the turn-based CGSs-is considered. In any location of these models (named TB-CGS hereafter), only one player has several moves (the other players have only one possible choice). Such models have the property of determinedness: given a set of players A, either there is a strategy for A to win some objective Φ, or there is a strategy for other players (Agt\A) to enforce ¬Φ. In such systems, modality R can be expressed as follows: A ϕ R ψ ≡ TB-CGS ¬ Agt\A (¬ϕ) U (¬ψ).

Complexity of ATL model-checking

In this section, we establish the precise complexity of ATL model-checking. All the complexity results below are stated for ATL but they are also true for ATL R .

Model-checking issues have been addressed in the seminal papers about ATL, on both ATSs [START_REF] Alur | Alternating-time temporal logic[END_REF] and CGSs [START_REF] Alur | Alternating-time temporal logic[END_REF]. The time complexity is shown to be in O(m • l), where m is the size of the transition table and l is the size of the formula. The authors then claim that the model-checking problem is in PTIME (and obviously, PTIME-complete). However, it is well-known (and already explained in [START_REF] Alur | Alternating-time temporal logic[END_REF][START_REF] Alur | Alternating-time temporal logic[END_REF]) that the size m of the transition table may be exponential in the number of agents. Thus, when the transition table is not given explicitly (as is the case for ATS), the algorithm requires in fact exponential time.

Before proving that this problem is indeed not in PTIME, we define the model of implicit CGSs, with a succinct representation of the transition table [START_REF] Jamroga | Do agents make model checking explode (computationally)?[END_REF]. Besides the theoretical aspect, it may be quite useful in practice since it allows to not explicitly describe the full transition table.

Explicit-and implicit CGSs

We distinguish between two classes of CGSs: Definition 8. • An explicit CGS is a CGS where the transition table is defined explicitly.

• An implicit CGS is a CGS where, in each location , the transition function is defined by a finite sequence ((ϕ 0 , 0 ), ..., (ϕ n , n )), where i ∈ Loc is a location, and ϕ i is a boolean combination of propositions A j = c that evaluate to true iff agent A i chooses move c. The transition table is then defined as follows: Edg( , m A1 , ..., m A k ) = j iff j is the lowest index s.t. ϕ j evaluates to true when players A 1 to A k choose moves m A1 to m A k . We require that the last boolean formula ϕ i be , so that no agent can enforce a deadlock.

The size |C| of a CGS C is defined as |Loc| + |Edg|. For explicit CGSs, |Edg| is the size of the transition table. For implicit CGSs, |Edg| is the sum |ϕ| used for the definition of Edg. See Appendix B for a discussion on the succinctness of the different models.

The size of an ATS is |Loc| + |Mov| where |Mov| is the sum of the number of locations in each possible move of each agent in each location.

Expressiveness of CGSs and ATSs

We prove in this section that CGSs and ATSs are closely related: they can model the same concurrent games. In order to make this statement formal, we use the following definition: Definition 9 ( [START_REF] Alur | Alternating refinement relations[END_REF]). Let A and B be two models of concurrent games (either ATSs or CGSs) over the same set Agt of agents. Let R ⊆ Loc A × Loc B be a (non-empty) relation between states of A and states of B. That relation is an alternating bisimulation when, for any ( , ) ∈ R, the following conditions hold:

-Lab A ( ) = Lab B ( ); for any coalition A ⊆ Agt, we have

∀m : A → Mov A ( , A). ∃m : A → Mov B ( , A). ∀q ∈ Next( , A, m ). ∃q ∈ Next( , A, m). (q, q ) ∈ R.
symmetrically, for any coalition A ⊆ Agt, we have

∀m : A → Mov B ( , A). ∃m : A → Mov A ( , A). ∀q ∈ Next( , A, m). ∃q ∈ Next( , A, m ). (q, q ) ∈ R.
where Next( , A, m) is the set of locations that are reachable from when each player A i ∈ A plays m(A i ).

Two models are said to be alternating-bisimilar if there exists an alternating bisimulation involving all of their locations.

With this equivalence in mind, ATSs and CGSs (both implicit and explicit ones) have the same expressive power: Theorem 10. 1. Any explicit CGS can be translated into an alternating-bisimilar implicit one in linear time; 2. Any implicit CGS can be translated into an alternating-bisimilar explicit one in exponential time; 3. Any explicit CGS can be translated into an alternating-bisimilar ATS in cubic time; 4. Any ATS can be translated into an alternating-bisimilar explicit CGS in exponential time; 5. Any implicit CGS can be translated into an alternating-bisimilar ATS in exponential time; 6. Any ATS can be translated into an alternating-bisimilar implicit CGS in quadratic time; Figure 4 summarizes those results. From our complexity results (and the assumption that the polynomial-time hierarchy does not collapse), the costs of the above translations is optimal. Those translations are detailled in Appendix B.

Model checking ATL on implicit CGSs.

Basically, the algorithm for model-checking ATL [2, 3] is similar to that for CTL: it consists in recursively computing fixpoints, based e.g. on the following equivalence:

A p U q ≡ µZ.(q ∨ (p ∧ A X Z))

ATS explicit CGS implicit CGS ( 4 ) e x p o n e n t i a l ( 3 ) c u b i c ( 6 ) q u a d r a t i c ( 5 ) e x p o n e n t i a l The difference with CTL is that we have to compute the pre-image of a set of states for some coalition.

It has been remarked in [START_REF] Jamroga | Do agents make model checking explode (computationally)?[END_REF] that computing the pre-images is not in PTIME anymore when considering implicit CGSs: the algorithm has to non-deterministically guess the moves of players in A in each location, and for each pre-image, to solve the resulting SATqueries derived from those choices and from the transition table. As a consequence, model-checking ATL on implicit CGSs is Σ P 2 -hard [START_REF] Jamroga | Do agents make model checking explode (computationally)?[END_REF]. However (see below), the Σ P 2 -hardness proof can very easily be adapted to prove Π P 2 -hardness. It follows that the Σ P 2 algorithm proposed in [START_REF] Jamroga | Do agents make model checking explode (computationally)?[END_REF] cannot be correct. The flaw is in the way it handles negation: games played on CGSs (and ATSs) are generally not determined, and the fact that a player has no strategy to enforce ϕ does not imply that the other players have a strategy to enforce ¬ϕ. It rather means that the other players have a co-strategy to enforce ¬ϕ (see [START_REF] Goranko | Complete axiomatization and decidability of alternating-time temporal logic[END_REF] for precise explanations about co-strategies).

Still, the Σ P 2 -algorithm is correct for formulas whose main operator is not a negation. As a consequence: Proposition 11. Model checking ATL on implicit CGSs is in ∆ P 3 .

Since the algorithm consists in labeling the locations with the subformulae it satisfies, that complexity holds even if we consider the DAG-size of the formula.

Before proving optimality, we briefly recall the Σ P 2 -hardness proof of [START_REF] Jamroga | Do agents make model checking explode (computationally)?[END_REF]. It relies on the following Σ P 2 -complete problem: EQSAT 2 : Input: two families of variables X = {x 1 , ..., x n } and Y = {y 1 , ..., y n }, a boolean formula ϕ on the set of variables X ∪ Y . Output: True iff ∃X. ∀Y. ϕ. This problem can be encoded in an ATL model-checking problem on an implicit CGS: the CGS has three states q 1 , q and q ⊥ , and 2n agents A 1 , ..., A n , B 1 , ..., B n , each having two possible choices in q 1 and only one choice in q and q ⊥ . The transitions out of q and q ⊥ are self loops. The transitions from q 1 are given by: δ(q 1 ) = ((ϕ[x j ← (A j ? = 1), y j ← (B j ? = 1)], q )( , q ⊥ )).

Then clearly, the coalition A 1 , ..., A n has a strategy for reaching q , i.e., q 1 |= A 1 , ..., A n X q , iff there exists a valuation for variables in X s.t. ϕ is true whatever B-agents choose for Y . Now, this encoding can easily be adapted to the dual (thus Π P 2 -complete) problem AQSAT 2 , in which, with the same input, the output is the value of ∀X. ∃Y. ϕ. It suffices to consider the same implicit CGS, and the formula ¬ A 1 , ..., A n X ¬q . It states that there is no strategy for players A 1 to A n to avoid q : whatever their choice, players B 1 to B n can enforce ϕ.

Following the same idea, we prove the following result:

Proposition 12. Model checking ATL on implicit CGSs is ∆ P 3 -hard.

Proof. We consider the following ∆ P 3 -complete problem [START_REF] Laroussinie | Model checking CTL + and FCTL is hard[END_REF][START_REF] Schobbens | Alternating-time logic with imperfect recall[END_REF].

SNSAT 2 : Input: m families of variables X i = {x 1 i , ..., x n i }, m families of variables Y i = {y 1 i , ..., y n i }, m variables z i , m boolean formulae ϕ i , with ϕ i involving variables in X i ∪ Y i ∪ {z 1 , ..., z i-1 }. Output: The value of z m , defined by          z 1 def = ∃X 1 . ∀Y 1 . ϕ 1 (X 1 , Y 1 ) z 2 def = ∃X 2 . ∀Y 2 . ϕ 2 (z 1 , X 2 , Y 2 ) . . . z m def = ∃X m . ∀Y m . ϕ m (z 1 , ..., z m-1 , X m , Y m )
We pick an instance I of this problem, and reduce it to an instance of the ATL model-checking problem. Note that such an instance uniquely defines the values of variables z i . We write v I : {z 1 , ..., z m } → { , ⊥} for this valuation. Also, when v I (z i ) = , there exists a witnessing valuation for variables in X i . We extend v I to {z 1 , ..., z m } ∪ i X i , with v I (x j i ) being a witnessing valuation if v I (z i ) = . We now define an implicit CGS C as follows: it contains mn agents A j i (one for each x j i ), mn agents B j i (one for each y j i ), m agents C i (one for each z i ), and one extra agent D. The structure is made of m states q i , m states q i , m states s i , and two states q and q ⊥ . There are three atomic propositions: s and s ⊥ , that label the states q and q ⊥ resp., and an atomic proposition s labeling states s i . The other states carry no label.

Except for D, the agents represent booleans, and thus always have two possible choices (0 and 1). Agent D always has m choices (0 to m -1). The transition relation is defined as follows: for each i, δ(q i ) = (( , s i )); δ(s i ) = (( , q i )); δ(q ) = (( , q )); δ(q ⊥ ) = (( , q ⊥ ));

δ(q i ) =           ((D ? = 0) ∧ ϕ i [x j i ← (A j i ? = 1
),

y j i ← (B j i ? = 1), z k ← (C k ? = 1)], q ) ((D ? = 0), q ⊥ ) ((D ? = k) ∧ (C k ? = 1), q k ) for each k < i ((D ? = k) ∧ (C k ? = 0), q k ) for each k < i ( , q )          
Intuitively, from state q i , the boolean agents chose a valuation for the variable they represent, and agent D can either choose to check if the valuation really witnesses ϕ i (by choosing move 0), or "challenge" player C k , with move k < i.

The ATL formula is built recursively by ψ 0 = and, writing AC for the coalition {A 1 1 , ..., A n m , C 1 , ..., C m }: ψ k+1 def = AC (¬s) U (q ∨ EX (s ∧ EX ¬ψ k )). Let f I (A) be the state-based strategy for agent A ∈ AC that consists in playing according to the valuation v I (i.e. move 0 if the variable associated with A evaluates to 0 in v I , and move 1 otherwise). The following lemma (proved in Appendix C) completes the proof of Proposition 12: Lemma 13. For any i ≤ m and k ≥ i, the following three statements are equivalent: (a) C, q i |= ψ k ; (b) the strategies f I witness the fact that C,

q i |= ψ k ; (c) variable z i evaluates to in v I .
With Proposition 11, this implies: Theorem 14. Model checking ATL on implicit CGSs is ∆ P 3 -complete.

Model checking ATL on ATSs.

For ATSs also, the PTIME upper bound only holds when the number of agents is fixed. As in the previous section, the NP algorithm proposed in [START_REF] Jamroga | Do agents make model checking explode (computationally)?[END_REF] for ATL model-checking on ATSs does not handle negation correctly. Again, the algorithm consists in computing fixpoints with pre-images, and the pre-images are now computed in NP [START_REF] Jamroga | Do agents make model checking explode (computationally)?[END_REF]. This yields a ∆ P 2 algorithm for full ATL. Proposition 15. Model checking ATL over ATSs is in ∆ P 2 . The NP-hardness proof of [START_REF] Jamroga | Do agents make model checking explode (computationally)?[END_REF] can be adapted in order to give a direct reduction of 3SAT, and then extended to SNSAT:

Proposition 16. Model checking ATL on ATSs is ∆ P 2 -hard.
Proof. Let us first recall the definition of the SNSAT problem [START_REF] Laroussinie | Model checking CTL + and FCTL is hard[END_REF]:

SNSAT:

Input: p families of variables X r = {x 1 r , ..., x m r }, p variables z r , p boolean formulae ϕ r in 3-CNF, with ϕ r involving variables in X r ∪ {z 1 , ..., z r-1 }. Output: The value of z p , defined by

               z 1 def = ∃X 1 . ϕ 1 (X 1 ) z 2 def = ∃X 2 . ϕ 2 (z 1 , X 2 ) z 3 def = ∃X 3 . ϕ 3 (z 1 , , z 2 , X 3 ) . . . z p def = ∃X p . ϕ p (z 1 , ..., z p-1 , X p )
Let I be an instance of SNSAT, where we assume that each ϕ r is made of n clauses S 1 r to S n r , with S j r = α j,1 r s j,1 r ∨ α j,2 r s j,2 r ∨ α j,3 r s j,3 r . Again, such an instance uniquely defines a valuation v I for variables z 1 to z r , that can be extended to the whole set of variables by choosing a witnessing valuation for x 1 r to x n r when z r evaluates to true.

We now describe the ATS A: it contains (8n + 3)p states: p states q r and p states q r , p states s r , and for each formula ϕ r , for each clause S j r of ϕ r , eight states q j,0 r , ..., q j,7 r , as in the previous reduction. States s r are labelled with the atomic proposition s, and states q j,k r that do not correspond to clause S j r are labeled with α. There is one player A j r for each variable x j r , one player C r for each z r , plus one extra player D. As regards transitions, there are self-loops on each state q j,k r , single transitions from each q r to the corresponding s r , and from each s r to the corresponding q r . From state q r , player A j r will choose the value of variable x j r , by selecting one of the following two sets of states:

{q g,k r | ∀l ≤ 3. s g,l r = x j r or α g,l r = 0} ∪ {q t , q t | t < r} if x j r = {q g,k r | ∀l ≤ 3. s g,l r = x j r or α g,l r = 1} ∪ {q t , q t | t < r} if x j r = ⊥
Both choices also allow to go to one of the states q t or q t . In q r , players A j t with t = r have one single choice, which is the whole set of states. player C t also chooses for the value of the variable it represents. As for players A j r , this choice will be expressed by choosing between two sets of states corresponding to clauses that are not made true. But as in the proof of Prop. 12, players C t will also offer the possibility to "verify" their choice, by going either to state q t or q t . Formally, this yields two sets of states:

{q g,k r | ∀l ≤ 3. s g,l r = z t or α g,l r = 0} ∪ {q u , q u | u = t} ∪ {q t } if z t = {q g,k r
| ∀l ≤ 3. s g,l r = z t or α g,l r = 1} ∪ {q u , q u | u = t} ∪ {q t } if z t = ⊥ -Last, player D chooses either to challenge a player C t , with t < r, by choosing the set {q t , q t }, or to check that a clause S j r is fulfilled, by choosing {q j,0 r , ..., q j,7 r }. Let us first prove that any choices of all the players yields exactly one state. It is obvious except for states q r . For a state q r , let us first restrict to the choices of all the players A j r and C r , then: if we only consider states q 1,0 r to q n,7 r , the same argument as in the previous proof ensures that precisely on state per clause is chosen, if we consider states q t and q t , the choices of players B t ensure that exactly one state has been chosen in each pair {q t , q t }, for each t < r.

Clearly, the choice of player D will select exactly one of the remaining states. Now, we build the ATL formula. It is a recursive formula (very similar to the one used in the proof of Prop. 12), defined by ψ 0 = and (again writing AC for the set of players {A 1 1 , ..., A m p , C 1 , ..., C p }):

ψ r+1 def = AC (¬s) U (α ∨ EX (s ∧ EX ¬ψ r )).
Then, writing f I for the state-based strategy associated to v I :

Lemma 17. For any r ≤ p and t ≥ r, the following statements are equivalent: (a) q r |= ψ t ; (b) the strategies f I witness the fact that q r |= ψ t ; (c) variable z r evaluates to true in v I .

The technical proof of this lemma is given in Appendix D. In the end:

Theorem 18. Model checking ATL on ATSs is ∆ P 2 -complete.

Model checking ATL +

The complexity of model checking ATL + over ATSs has been settled ∆ P 3 -complete in [START_REF] Schobbens | Alternating-time logic with imperfect recall[END_REF]. But ∆ P 3 -hardness proof of [START_REF] Schobbens | Alternating-time logic with imperfect recall[END_REF] is in LOGSPACE only w.r.t. the DAG-size of the formula. We prove (in Appendix E) that model checking ATL + is in fact ∆ P 3 -complete (with the standard definition of the size of a formula) for our three kinds of game structures.

Theorem 19. Model checking ATL + is ∆ P 3 -complete on ATSs as well as on explicit CGSs and implicit CGSs.

Conclusion

In this paper, we considered the basic questions of expressiveness and complexity of ATL. We showed that ATL, as originaly defined in [START_REF] Alur | Alternating-time temporal logic[END_REF][START_REF] Alur | Alternating-time temporal logic[END_REF], is not as expressive as it could be expected, and we argue that the modality "Release" should be added in its definition [START_REF] Jamroga | Model checking abilities of agents: A closer look[END_REF].

We also precisely characterized the complexity of ATL and ATL + modelchecking, on both ATSs and CGSs, when the number of agents is not fixed. These results complete the previously known results about these formalisms and it is interesting to see that their complexity classes (∆ P 2 or ∆ P 3 ) are unusual in the model-checking area.

As future works, we plan to focus on the extensions EATL (extending ATL with a modality • ∞ F , and for which state-based strategies are still sufficient) and EATL + (the obvious association of both extensions, but for which statebased strategies are not sufficient anymore).

A Proof of Lemma 6 Lemma 6. Consider the CGS C displayed at Fig. 3. For any i > 0, for any

ψ ∈ ATL with |ψ| ≤ i, b i |= ψ iff b i+1 |= ψ (2)
s i |= ψ iff s i+1 |= ψ (3)
s i |= ψ iff s i+1 |= ψ (4)
Proof. The proof proceeds by induction on i, and on the structure of the formula ψ.

Base case: i = 1. Since we require that |ψ| ≤ i, ψ can only be an atomic proposition. The result is then obvious.

Induction step. We assume the result holds up to some i -1 ≥ 1, and prove that it then still holds for i. Let ψ s.t. |ψ| ≤ i. We now proceed by structural induction on ψ:

-The result is again obvious for atomic propositions, as well as for boolean combinations of subformulae. -Otherwise, the "root" combinator of ψ is a modality. If it is a CTL modality, the results are quite straightforward. Also, since there is only one transition from b i , any ATL modality can be expressed as a CTL modality in that state, and

-If ψ = A 1 X ψ 1 : Assume s i |= ψ. Then, depending on the strategy, either b i and s i-1 , or a i and s i-1 , or s i and s i-1 , should satisfy ψ 1 . By i.h., this propagates to the next level, and the same strategy can be mimicked from s i+1 . The converse is similar (hence (3)), as well as the proof for (4). -If ψ = A 1 G ψ 1 : If s i |= ψ, then s i , thus s i+1 , satisfy ψ 1 . Playing move 3 is a strategy for player A 1 to enforce G ψ 1 from s i+1 , since the game will either stay in s i+1 or go to s i , where player A has a winning strategy. The converse is immediate, since player A 1 cannot avoid s i when playing from s i+1 . Hence (3) for A 1 G -formulae.

If s i |= ψ, then both s i and s i+1 satisfy ψ 1 . Also, player A 1 cannot avoid the play to go in location s i-1 . Thus, s i-1 |= ψ 1 -and by i.h., so does s iand s i |= ψ, as above. Now, following the same strategy in s i+1 as the winning strategy of s i clearly enforces G ψ 1 . The converse is similar: it suffices to mimic, from s i , the strategy witnessing the fact that s i+1 |= ψ. This proves (4), and concludes this case.

-If ψ = A 1 ψ 1 U ψ 2 : If s i |= ψ, then either ψ 2 or ψ 1 holds in s i , thus
in s i+1 . The former case is trivial. In the latter, player A 1 can mimic the winning strategy in s i+1 : the game will end up in s i , with intermediary states satisfying ψ 1 (or ψ 2 ), and he can then apply the original strategy.

The converse is obvious, since from s i+1 , player A 1 cannot avoid location s i , from which he must also have a winning strategy.

If s i |= ψ, omitting the trivial case where s i satisfies ψ 2 , we have that s i-1 |= ψ. Also, a (state-based) strategy in s i witnessing ψ necessary consists in playing move 1 or 2. Thus a i and b i satisfy ψ, and the same strategy (move 1 or 2, resp.) enforces G ψ 1 from s i . It is now easy to see that the same strategy is correct from s i+1 . Conversely, apart from trivial cases, the strategy can again only consists in playing moves 1 or 2. In both cases, the game could end up in s i , and then in s i-1 . Thus s i-1 |= ψ, and the same strategy as in s i+1 can be applied in s i to witness ψ. -The proofs for A 2 X ψ 1 , A 2 X ψ 1 , and A 2 ψ 1 U ψ 2 are very similar to the previous ones.

B From ATSs to CGSs

Theorem 10. 1. An explicit CGS can be translated into an alternating-bisimilar implicit one in linear time; 2. An implicit CGS can be translated into an alternating-bisimilar explicit one in exponential time; 3. An explicit CGS can be translated into an alternating-bisimilar ATS in cubic time; 4. An ATS can be translated into an alternating-bisimilar explicit CGS in exponential time; 5. An implicit CGS can be translated into an alternating-bisimilar ATS in exponential time; 6. An ATS can be translated into an alternating-bisimilar implicit CGS in quadratic time;

Proof. Points 1, 2, and 4 are reasonnably easy.

For point 6, it suffices to write, for each possible next location, the conjunction (on each agent) of the disjunction of the choices that contain that next location. For instance, if we have Mov A ( 0 , A 1 ) = {{ 1 , 2 }, { 1 , 3 }} and Mov A ( 0 , A 2 ) = {{ 2 , 3 }, { 1 }} in the ATS A, then each player will have two choices in the associated CGS B, and

Edg B ( 0 ) =   (A 1 = 1 ∨ A 1 = 2) ∧ (A 2 = 2), 1 (A 1 = 1) ∧ (A 2 = 1), 2 (A 1 = 2) ∧ (A 2 = 1), 3  
Formally, let A = (Agt, Loc A , AP, Lab A , Mov A ) be an ATS. We then define B = (Agt, Loc B , AP, Lab B , Mov B , Edg B ) as follows:

-Loc B = Loc A , Lab B = Lab A ; -Mov B : × A i → [1, |Mov A ( , A i )|];
-Edg B is a function mapping each location to the sequence ((ϕ , )) ∈Loc A (the order is not important here, as the formulas will be mutually exclusive) with It is now easy to prove that the identity Id ⊆ Loc A × Loc B is an alternating bisimulation, since there is a direct correspondance between the choices in both structures.

We now explain how to transform an explicit CGS into an ATS, showing point 3. Let A = (Agt, Loc A , AP, Lab A , Mov A , Edg A ) be an explicit CGS. We define the ATS B = (Agt, Loc B , AP, Lab B , Mov B ) as follows (see Figure 5 for more intuition on the construction): It is now only a matter of bravery to prove that R is an alternating bisimulation between A and B.

-Loc B ⊆ Loc A ×Loc A ×N k ,
Point 5 is now immediate (through explicit CGSs), but it could also be proved in a similar way as point 3.

Let us mention that our translations are optimal (up to a polynomial): our exponential translations cannot be achieved in polynomial time because of our complexity results for ATL model-checking. Note that it does not mean that the resulting structures must have exponential size. Moves from location A: Player 1 move 1: {ba,1,1, da,1,2, da,1,3} move 2: {ca,2,2, ca,2,3, da,2,1} move 3: {aa,3,1, da,3,2, da,3,3} Player 2 move 1: {aa,3,1, ba,1,1, da,2,1} move 2: {ca,2,2, da,1,2, da,3,2} move 3: {ca,2,3, da,1,3, da,3,3}

C Proof of Lemma 13

  t. (1) M |= Φ, (2) M |= Φ, and (3) M and M satisfy the same ATL formula.

Fig. 4 .

 4 Fig. 4. Costs of translations between the three models

  Computing Edg B requires quadratic time (more precisely O(|Loc A | × |Mov A |)).

  where k = |Agt|, with ( , , m A1 , . . . , mA k ) ∈ Loc B iff = Edg A ( , m A1 , . . . , m A k ); -Lab B ( , , m A1 , . . . , m A k ) = Lab A ( ); -From a location q = ( , , m A1 , . . . , m A k ), player A j has |Mov A ( , A j )| possible moves: Mov B (q, A j ) = ( , , m A1 , . . . , m Aj = i, . . . , m A k ) | m An ∈ Mov A ( , A n ) and = Edg A ( , m A1 , . . . , m Aj = i, . . . , m A k ) | i ∈ Mov A ( , A j ) This ATS is built in time O(|Loc A | 2 • |Edg A |).It remains to show alternating bisimilarity between those structures. We define the relation R = {( , ( , , m A1 , . . . , m A k )) | ∈ Loc A , ( , , m A1 , . . . , m A k )) ∈ Loc B }.

Lemma 13 .

 13 For any i ≤ m and k ≥ i, the following three statements are equivalent:

Fig. 5 .

 5 Fig. 5. Converting an explicit CGS into an ATS

We adopt the classical hypothesis that the polynomial-time hierarchy does not collapse, and that PTIME = NP. We refer to[START_REF] Ch | Computational Complexity[END_REF] for the definitions about complexity classes, especially about oracle Turing machines and the polynomial-time hierarchy.

I.e., fA i ( 0 • • • m) ∈ Mov( m, Ai).

We might omit to mention S when it is clear from the context.

This formula can also be written A a W b, where W is the "weak until" modality.

Given the translation from CGS to ATS (see Section 4.2), the result also holds for ATSs.

Acknowledgement. We thank Wojtek Jamroga for pointing out that formulas in SNSAT 2 cannot be restricted to CNF [6].

Proof. Clearly, (b) implies (a). We prove that (a) implies (c) and that (c) implies (b) by induction on i.

First assume that q 1 |= ψ j , for some j ≥ 1. Since only q and q ⊥ are reachable from q 1 , we have q 1 |= AC X q . We are (almost) in the same case as in the Σ P 2 reduction of [START_REF] Jamroga | Do agents make model checking explode (computationally)?[END_REF]: there is a valuation of the variables x 1 1 to x n 1 s.t., whatever players D and B 1 1 to B n m decide, the run will end up in q . This holds in particular if player D chooses move 0: for any valuation of the variables y 1 1 to y n 1 , ψ 1 (X 1 , Y 1 ) holds true, and z 1 evaluates to true in v I .

Secondly, if z 1 evaluates to true, then v I (x 1 1 ), ..., v I (x n 1 ) are such that, whatever the value of y 1 1 to y n 1 , ψ 1 holds true. If players A 1 1 to A n 1 play according to f I , then players D and B 1 1 to B n 1 cannot avoid state q , and q 1 |= AC X q , thus also ψ k when k ≥ 1.

We now assume the result holds up to index i ≥ 1, and prove that it also holds at step i + 1. Assume q i+1 |= ψ k+1 , with k ≥ i. There exists a strategy witnessing ψ k+1 , i.e., s.t. all the outcomes following this strategy satisfy (¬s) U (q ∨ EX (s∧ EX ¬ψ k )). Depending on the move of player D in state q i+1 , we get several informations: first, if player D plays move l, with 1 ≤ l ≤ i, the play goes to state q l or q l , depending on the choice of player C l .

if player C l chose move 0, the run ends up in q l . Since the only way out of that state is to enter state s l , labeled by s, we get that q l |= EX (s ∧ EX ¬ψ k ), i.e., that q l |= ¬ψ k . By i.h., we get that z l evaluates to false in our instance of SNSAT 2 . if player C l chose move 1, the run goes to q l . In that state, players in AC can keep on applying their strategy, which ensures that q l |= ψ k+1 , and, by i.h., that z l evaluates to true in I.

Thus, the strategy for AC to enforce ψ k+1 in q i+1 requires players C 1 to C i to play according to v I and the validity of these choices can be verified by the "opponent" D. Now, if player D chooses move 0, all the possible outcomes will necessarily immediately go to q (since ψ k+1 holds, and since q ⊥ |= EX (s ∧ EX ¬ψ k )). We immediately get that players B 1 i+1 to B n i+1 cannot make ψ i+1 false, hence that z i+1 evaluates to true in I.

Secondly, if z i+1 evaluates to true, assume players in AC play according to f I , and consider the possible moves of player D:

if player D chooses move 0, since z i+1 evaluates to true and since players C 1 to C i and A 1 i+1 to A n i+1 have played according v I , there is no way for player B 1 i+1 to B n i+1 to avoid state q . if player D chooses some move l between 1 and i, the execution will go into state q l or q l , depending on the move of C l .

• if C l played move 0, i.e., if z l evaluates to false in v I , the execution goes to state q l , and we know by i.h. that q l |= ¬ψ k . Thus q l |= EX (s∧ EX ¬ψ k ), and the strategy still fulfills the requirement. • if C l played move 1, i.e., if z l evaluates to true, then the execution ends up in state q l , in which, by i.h., the strategy f I enforces ψ k+1 . if player D plays some move l with l > i, the execution goes directly to q , and the formula is fulfilled.

D Proof of Lemma 17

Lemma 17. For any r ≤ p and t ≥ r, the following statements are equivalent:

(a) q r |= ψ t ; (b) the strategies f I witness the fact that q r |= ψ t ; (c) variable z r evaluates to true in v I .

Proof. We prove by induction on r that (a) implies (c) and that (c) implies (b), the last implication being obvious. For r = 1, since no s-state is reachable, it amounts to the previous proof of NP-hardness.

Assume the result holds up to index r. Then, if q r+1 |= ψ t+1 for some t ≥ r, we pick a strategy for coalition AC witnessing this property. Again, we consider the different possible choices available to player D:

if player D chooses to go to one of q u and q u , with u < r + 1: the execution ends up in q u if player C u chose to set z u to true. But in that case, formula ψ t+1 still holds in q u , which yields by i.h. that z u really evaluates to true in v I . Conversely, the execution ends up in q u if player C u set z u to false. In that case, we get that q u |= ¬ψ t , with t ≥ u, which entails by i.h. that z u evaluates to false. This first case entails that player C 1 to C r chose the correct value for variables z 1 to z r . if player D chooses a set of eight states corresponding to a clause S j r+1 , then the strategy of other players ensures that the execution will reach a state labeled with α. As in the previous reduction, this indicates that the corresponding clause has been made true by the choices of the other players.

Putting all together, this proves that variable z r+1 evaluates to true. Now, if variable z r+1 evaluates to true, Assume the players in AC play according to valuation f I . Then if player D chooses to go to a set of states that correspond to a clause of ϕ r+1 , he will necessarily end up in a state that is labeled with α, since the clause is made true by the valuation we selected. if player D chooses to go to one of q u or q u , for some u, then he will challenge player B u to prove that his choice was correct. By i.h., and since player B u played according to f I , formula (¬s) U (α ∨ EX (s ∧ EX ¬ψ t+1 )) will be satisfied, for any t ≥ u.

E Complexity of model checking ATL +

Proposition 20. Model checking ATL + can be achieved in ∆ P 3 on implicit CGSs.

Proof. A ∆ P 3 algorithm is given in [START_REF] Schobbens | Alternating-time logic with imperfect recall[END_REF] for explicit CGSs. We extend it to handle implicit CGSs: for each subformula of the form A ϕ, guess (state-based) strategies for players in A. In each state, the choices of each player in A can be replaced in the transition functions. We then want to compute the set of states where the CTL + formula Aϕ holds. This can be achieved in ∆ P 2 [START_REF] Clarke | Automatic verification of finitestate concurrent systems using temporal logic specifications[END_REF][START_REF] Laroussinie | Model checking CTL + and FCTL is hard[END_REF], but requires to first compute the possible transitions in the remaining structure, i.e., to check which of the transition formulae are satisfiable. This is done by a polynomial number of independent calls to an NP oracle, and thus does not increase the complexity of the algorithm. Proof. This reduction is a quite straightforward extension of the one presented in [START_REF] Laroussinie | Model checking CTL + and FCTL is hard[END_REF] for CTL + . In particular, it is quite different from the previous reductions, since the boolean formulae are now encoded in the ATL + formula, and not in the model. We encode an instance I of SNSAT 2 , keeping the notations used in the proofs of Prop. 12 (for the SNSAT 2 problem) and 16 (for clause numbering). Fig. 6 depicts the turn-based two-player CGS C associated to I. States s 1 to s m are labeled by atomic proposition s, states z 1 to z m are labeled by atomic proposition z, and the other states are labeled by their name as shown on Fig. 6.

The ATL + formula is built recursively, with ψ 0 = and

where l j,k w = v when s j,k w = v and α j,k w = 1, and l j,k w = v when s j,k w = v and α j,k w = 0. We then have: Lemma 22. For any r ≤ p and t ≥ r, the following statements are equivalent: When r = 1, since no s-or z-state is reachable from z 1 , the fact that z

1 . This in turn is equivalent to the fact that z 1 evaluates to true in I.

We now turn to the inductive case. If z r+1 |= ψ t+1 with t ≥ r, consider a strategy for A s.t. all the outcomes satisfy the property, and pick one of those outcomes, say ρ. Since it cannot run into any s-state, it defines a valuation v ρ for variables z 1 to z r+1 and x 1 1 to x n m in the obvious way. Each time the outcome runs in some z u -state, it satisfies EX (s ∧ EX ψ t ). Each time it runs in some z ustate, the suffix of the outcome witnesses formula ψ t+1 in z u . Both cases entail, thanks to the i.h., that v ρ (z u ) = v I (z u ) for any u < r + 1. Now, the subformula w [(F z w ) → j≤n k≤3 F l j,k w , when w = r + 1, entails that ϕ r+1 is indeed satisfied whatever the values of the y j r+1 's, i.e., that z r+1 evaluates to true in I. Conversely, if z r evaluates to true, then strategy f I clearly witnesses the fact that ψ t holds in state z r .