Comparing Variants of Strategic Ability

1 Introduction

Alternating-time temporal logic (ATL) [3] is a temporal logic that incorporates some basic game theoretical notions. Semantic variants of ATL are usually derived from different assumptions about agents' capabilities. Can the agents "see" the current state of the system, or only a part of it? Can they memorize the whole history of observations in the game? Is it enough that they have a way of enforcing the required temporal property "objectively", or should they be able to come up with the right strategy on their own? Different answers to these questions induce different semantics of strategic ability, and they clearly give rise to different analyses of a given problem domain. However, it is not entirely clear to what extent they give rise to different logics. One natural question that arises in this respect is whether these semantic variants generate different sets of valid (and, dually, satisfiable) sentences. In this paper, we settle the issue and show that most "classical" semantic variants of ATL are indeed different, and we characterize the relationship between their sets of validities.

The question is important for several reasons. First, by comparing validity sets we compare the respective logics in the traditional sense. Moreover, validities of ATL capture general properties of games under consideration: if, e.g., two variants of ATL generate the same valid sentences then the underlying notions of ability induce the same kind of games. All the variants studied here are defined over the same class of models that generalizes extensive games. The difference between games "induced" by different semantics lies in available strategies and the winning conditions for them.

Finally, the satisfiability problem for ATL, though far less studied than model checking, is not necessarily less important. While model checking ATL can be seen as the analogue of game solving, satisfiability corresponds naturally to mech-

Nils Bulling

Department of Informatics, Clausthal University of Technology, Germany

bulling@in.tu-clausthal.de

anism design. A systematic study on the abstract level is the first step towards algorithms that solve the problem.

Ultimately, we show that what agents can achieve is more sensitive to the strategic model of an agent (and a precise notion of achievement) than it was generally realized. No less importantly, our study reveals that some natural properties - usually taken for granted when reasoning about action - may cease to be universally true if we change the strategic setting. Examples include fixpoint characterizations of temporal/strategic operators (that enable incremental synthesis and iterative execution of strategies) and the duality between necessary and obtainable outcomes in a game.

Related Work. ATL has been studied extensively; however, most of the research was focused on the way such logics can be used for specification and verification of multi-agent systems. Semantic variants were defined that match various interpretations of ability [7; 12; 9], and the complexity of model checking was investigated and compared for different settings and different variants of the logic [12; 13; 8]. Axiomatization and satisfiability were investigated in [5; 15; 11], and expressivity issues were raised in [10]. Surprisingly, relationships between the "classical" semantic variants (as defined in [12]) have not yet been studied, though analogous results exist for more sophisticated variations (cf. [1] for irrevocable strategies and [2] for agents with bounded memory). In particular, formal properties of ATL variants for imperfect information were largely left untouched.

2 Reasoning about Strategic Abilities

ATL [3] generalizes the branching time logic CTL by replacing path quantifiers E, A 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: " ❣" ("in the next state"), "✷" ("always from now on") and U ("until"). The additional operator "✸" ("now or sometime in the future") can be defined as ✸γ ≡ ⊤U γ. Formally, the language of ATL∗ is given by the grammar below, where A is a set of agents, and p is an atomic proposition:

The best known syntactic variant of alternating time temporal logic is "ATL without star" (or "vanilla" ATL) in which every occurrence of a cooperation modality is uniquely coupled with a temporal operator. ATL+ sits between ATL∗ and "vanilla" ATL: it allows cooperation modalities to be followed by a Boolean combination of simple temporal subformulae. We will use the acronym ATL to refer to "ATL without star" when no confusion can arise.

2.1 Basic Semantics of ATL

In [3], the semantics of alternating-time temporal logic 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) 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 nonempty sets of actions available to agents at each state, and o is a (deterministic) transition function that assigns the outcome state q′ = o(q, α1, . . . , αk) to state q and a tuple of actions αi ∈ d(i, q) that can be executed by Agt in q.

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 ΛM(q). Moreover, we define Λf in M (q) as the set of all finite prefixes of ΛM(q).

In the standard version of ATL [3], strategies are represented by functions sa : St+ → Act. A collective strategy for a group of agents A = {a1, . . . , ar} is simply a tuple of individual strategies sA = 〈sa1 , . . . , sar 〉. The "outcome" function out(q, sA) returns the set of all paths that may occur when agents A execute strategy sA from state q onward. Now, the semantics of ATL∗ and its sublanguages can be defined by the standard clauses for Boolean and temporal operators, plus the following clause for 〈〈A〉〉 (cf. [3] for details):

• M, q |= 〈〈A〉〉γ iff there is a strategy sA for agents A such that for each path λ ∈ out(q, sA), we have M, λ |= γ.

Note that the semantics does not address the issue of coordination [4]: if there exist several successful strategies for A, the agents in A will somehow choose between them.

We recall that the following fixpoint properties are valid in the original semantics of ATL [3]:

Moreover, the path quantifiers A, E of CTL can be expressed in ATL with 〈〈∅〉〉, 〈〈Agt〉〉 respectively. As a consequence, the CTL duality axioms can be rewritten in ATL, and become validities in the basic semantics:

2.2 Between Uncertainty and Recall

A number of semantic variations have been proposed for ATL, cf. e.g. [7; 12; 9; 1; 2]. In this paper, we study the "canonical" variants as proposed in [12]. There, a taxonomy of four strategy types was introduced and labeled as follows: I

(resp. i) stands for perfect (resp. imperfect) information, and R (resp. r) refers to perfect recall (resp. no recall). The semantics of ATL can be parameterized with the strategy type - yielding four different semantic variants of the logic, labeled accordingly (ATLIR, ATLIr, ATLiR, and ATLir). In this paper, we extend the taxonomy with a distinction between objective and subjective abilities under imperfect information, denoted by io and is; the distinction can be traced back to [7; 9].

Models, imperfect information concurrent game structures (iCGS) [14; 12], are CGS's augmented with a family of indistinguishability 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′ of the system. Each ∼a is assumed to be an equivalence relation. It is also required that agents have the same choices in indistinguishable states: if q ∼a q′ then d(a, q) = d(a, q′ ). Note that CGS's can be seen as the subclass of iCGS's where all ∼a are the minimal reflexive reflexive relations.

A history is a finite sequence of states. 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 (i.e., q and q′ are indistinguishable for group A iff there is at least one agent in A for whom q and q′ look the same).

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

• Ir: sa : St →Act such that sa(q) ∈ d(a, q) for all q;
• IR: sa : St+ → Act such that sa(q0 . . . qn) ∈ d(a, qn) for all q0, . . . , qn;
• ir (i.e., isr or ior): like Ir, with the additional constraint that q ∼a q′ implies sa(q) = sa(q′ );
• iR (i.e., isR or ioR): like IR, with the additional constraint that h ≈a h′ implies sa(h) = sa(h′ ).

That is, strategy sa is a conditional plan that specifies a's action in each state of the system (for memoryless agents) or for every possible history of the system evolution (for agents with perfect recall). Moreover, imperfect information strategies specify the same choices for indistinguishable states (resp. histories). As before, collective xy-strategies sA are tuples of individual xy-strategies sa, one per a ∈ A.

The set of possible outcomes of a strategy is defined as:

• outxy (q, sA) = out(q, sA) for x ∈ {I, io} and y ∈ {r, R};
• outxy (q, sA) = ⋃q∼Aq′ out(q′ , sA) for x = is and y ∈ {r, R}.

We obtain the semantics for ATLxy by changing the clause for 〈〈A〉〉γ from Section 2.1 in the following way:

• M, q |=xy 〈〈A〉〉γ iff there is an xy-strategy sA such that for each λ ∈ outxy (q, sA), we have M, λ |=xy γ.

Note that the I and io semantics of ATL look only at outcome paths starting from the current global state of the system. In other words, they formalize the properties which agents can enforce objectively (but, in case of uncertainty about the current state, they may be unaware of the fact). In contrast, the is semantics of 〈〈A〉〉γ refers to all outcome paths starting from states that look the same as the current state for coalition A. Hence, it formalizes the notion of A knowing how to play in the sense that A can identify a single strategy that succeeds from all the states they consider possible. We follow [12] by taking the "everybody knows" interpretation of collective uncertainty. More general settings were proposed in [9]; we believe that the results in this paper carry over to the other cases of "knowing how to play", too.

We observe that the basic semantics of ATL from [3] corresponds exactly to ATLIR. Moreover, in "vanilla" ATL both semantics for perfect information coincide:

Proposition 1 ([3; 12]) For every iCGS M, state q, and ATL formula ϕ, we have that M, q |=IR ϕ iff M, q |=Ir ϕ.

3 Comparing Validities for Variants of ATL

In this section we present a formal comparison of the semantic variants defined in Section 2. As stated in the introduction, we compare the variants on the level of their validity sets (or, equivalently, satisfiable sentences). In most cases, they turn out to be different. Also, we can usually show that one variant is a refinement of the other in the sense that its set of validities strictly subsumes the validities induced by the other variant.

In what follows, we write Val(ATLsem) to denote the set of ATL validities under semantics sem. Likewise, we write Sat(ATLsem) for the set of ATL formulae satisfiable in sem. The conceptual reading of V al(ATLsem1) ⊊ V al(ATLsem2) can be as follows: for "game boards" given by iCGS's, we have that the "game rules" in semantics ATLsem1 strictly refine the rules in ATLsem2.

3.1 Perfect vs. Imperfect Information

We begin by comparing perfect and imperfect information scenarios. That is, in the first class (I), agents recognize the current global state of the system by definition. In the latter (i), uncertainty of agents about states constraints their choices.

Comparing ATLir vs. ATLIr

First, we observe that perfect information can be seen as a special case of imperfect information.

Proposition 2 Val (ATLisr) ⊆ Val (ATLIr) and Val (ATLior) ⊆ Val (ATLIr).

Proof. Since perfect information of agents can be explicitly represented in iCGS by fixing all relations ∼a as the minimal reflexive relations (q ∼a q′ iff q = q′ ), we have that ϕ ∈ Sat(ATLIr) implies ϕ ∈ Sat(ATLisr) and ϕ ∈ Sat(ATLior). Thus, dually, Val(ATLisr) ⊆ Val(ATLIr) and Val (ATLior) ⊆ Val (ATLIr). ■

Proposition 3 Val (ATLIr) ̸⊆ Val (ATLisr).

Proof. We show that by presenting a validity for ATLIr which is not valid in ATLisr. Consider the formula that captures the right-to-left direction in the fixpoint characterization of 〈〈a〉〉✸:

Φ1 is Ir-valid (cf. Section 2). To see its invalidity in the isr semantics, consider model M1 from Figure 1. 1 Indeed, for p ≡ shot, we get M1, q0 |=isr p ∨ 〈〈a〉〉 ❣〈〈a〉〉✸p and M1, q0 ̸|=isr 〈〈a〉〉✸p, which formally concludes our proof. ■

Proof. It is sufficient to show that Φ1 ≡ (p ∨ 〈〈a〉〉 ❣〈〈a〉〉✸p) → 〈〈a〉〉✸p is invalid in the ior semantics. Take model M2 in Figure 2 and p ≡ shot. Now we have that M2, q′0 |=ior p ∨ 〈〈a〉〉 ❣〈〈a〉〉✸p because a has a uniform strategy to achieve ✸p in q0 (sa(q) = shootL for every q) and another uniform strategy in q1 (s′a (q) = shootR for every q). However, sa and s′a cannot be merged into a single uniform strategy, and indeed M2, q′0 ̸|=ior 〈〈a〉〉✸p. ■

Corollary 1 Val (ATLisr) ⊊ Val (ATLIr) and Val (ATLior) ⊊ Val (ATLIr).

Comparing ATLiR vs. ATLIR

First, we observe that for ATLioR vs. ATLIR we can employ the same reasoning as for for ATLior vs. ATLIr. Abilities under perfect information can be still seen as a special case of imperfect information abilities, and we can use the same model M2 to invalidate the same formula Φ1 in ATLioR. Thus, analogously to Corollary 1 we get:

1 The story behind Figure 1 is as follows. A man wants to shoot down a yellow rubber duck in a shooting gallery. The man knows that the duck is in one of the two cells in front of him, but he does not know in which one. Moreover, this has been a long party, and he is very tired, so he is only capable of using memoryless strategies at the moment. Does he have a memoryless strategy which he knows will achieve the goal? No. He can either decide to shoot to the left, or to the right, or reach out to the cells and look what is in (note also that the cells close in the moment after being opened). In each of these cases the man risks that he will fail (at least from his subjective point of view). Does he have an opening strategy that he knows will guarantee his knowing how to shoot the duck in the next moment? Yes. The opening strategy is to look; if the system proceeds to q4 then the second strategy is to shoot to the left, otherwise the second strategy is to shoot to the right.

Corollary 2 Val (ATLioR) ⊊ Val (ATLIR).

By the same reasoning as above, Val(ATLisR) ⊆ Val(ATLIR). To settle the other direction, we need to use another counterexample, though.

Proof. This time we consider the other direction of the fixpoint characterization for 〈〈a〉〉✸:

Φ2 is IR-valid, but it is not valid in isR. Consider the "poor duck model" M1 from Figure 1 but without the transitions corresponding to look leading from state q0 to q4 and from q1 to q5. We call this model M ′1 and take p ≡ shot. Then, we have that M ′1 , q4 |=isR 〈〈a〉〉✸p, but M ′1 , q4 ̸|=isR p ∨ 〈〈a〉〉 ❣〈〈a〉〉✸p, which concludes the proof. ■

Corollary 3 Val(ATLisR) ⊊ Val(ATLIR) and Val(ATLisR) ⊊ Val (ATLIr).

3.2 Perfect Recall vs. Memoryless Strategies

Now we proceed to examine the impact of perfect vs. no recall on the general strategic properties of agent systems.

Comparing ATLIr vs. ATLIR

We have already mentioned that, in "vanilla" ATL, the Ir- and IR-semantics coincide (Proposition 1). As a consequence, they induce the same validities: Val (ATLIr) = Val (ATLIR). Thus, regardless of the type of their recall, perfect information agents possess the same abilities with respect to winning conditions that can be specified in "vanilla" ATL. An interesting question is: does it carry over to more general classes of winning conditions, or are there (broader) languages that can discern between the two types of ability? The answer is: yes, there are. The Ir- and IR-semantics induce different validity sets for ATL∗ , and in fact the distinction is already present in ATL+. Moreover, it turns out that perfect recall can be seen as a special case of memoryless play in the sense of their general properties.

Our proof of Proposition 6 draws inspiration from the proof of [1, Theorem 8.3]. We start with some additional notions and two useful lemmata.

Definition 1 (Tree-like CGS) Let M be a CGS and q be a state in it. M is called tree-like iff there is a state q (the root) such that for every q′ there is a unique finite sequence of states leading from q to q′ .

Definition 2 (Tree unfolding) Let M = (Agt, St,Π, π, Act, d, o) be a CGS and q be a state in it. The treeunfolding of M starting from state q denoted T(M, q) is defined as (Agt, St′ , Π, π′ , Act, d′ , o′ ) where St′ := Λfin M (q), d′ (a, h) := d(a, last(h)), o′ (h, ⃗α) := h ◦ o(last(h), ⃗α), and π′ (h) := π(last(h)).

Lemma 1 For every tree-like CGS M, state q in M, and ATL∗ formula ϕ, we have: M, q |=Ir ϕ iff M, q |=IR ϕ.

Proof sketch. Induction over the structure of ϕ. The main case is ϕ ≡ 〈〈A〉〉γ; to see that the proof goes through, observe that the subtree of M starting from q is also a tree-like CGS, and on tree-like CGS's Ir and IR strategies coincide. ■

Lemma 2 For every CGS M, state q in M, and ATL∗ formula ϕ, M, q |=IR ϕ iff T(M, q), q |=IR ϕ.

Proof sketch. Induction over the structure of ϕ. The main case is again ϕ ≡ 〈〈A〉〉γ for which it is sufficient to observe that (i) IR-strategies in M, q uniquely correspond to IR-strategies in T(M, q), q; (ii) outM(q, sA) = outT (M,q) (q, sA) for every IR strategy sA. ■

Proposition 6 Val (ATL∗Ir ) ⊆ Val (ATL∗IR )

Proof. Let an ATL∗ formula ϕ be Ir-valid in iCGS's, then it is also Ir-valid in tree-like CGS's, and by Lemma 1 also IRvalid in tree-like CGS's. Thus, by Lemma 2, it is IR-valid in arbitrary CGS's. Since indistinguishability relations do not influence |=IR, we get that ϕ is IR-valid in iCGS's. ■

In particular, the subsumption holds for formulae of ATL+. Moreover:

Proposition 7 Val (ATL+IR ) ̸⊆ Val (ATL+Ir ).

Proof. Consider formula

The formula is valid in ATL+IR [6]. On the other hand, its right-to-left part is not valid in ATL+Ir . To see this, we take the single-agent CGS M3 from Figure 3 where agent a (the robot) can either do the cleaning or the delivery of a package. Then, for p1 ≡ clean, p2 ≡ delivered, we have M3, q0 |=Ir 〈〈a〉〉✸(p1 ∧ 〈〈a〉〉✸p2 ∨ p2 ∧ 〈〈a〉〉✸p1) but also M3, q0 ̸|=Ir 〈〈a〉〉(✸p1 ∧ ✸p2). ■

Corollary 4 Val (ATL+Ir ) ⊊ Val (ATL+IR ).

Comparing ATLior vs. ATLioR and ATLisr vs. ATLisR

Now we compare the memoryless and perfect recall semantics under uncertainty.

Proof idea. The basic idea is similar to the one behind Proposition 6. First, we define ioR-tree unfoldings of iCGS's - similar to unfoldings of CGS's but extended with indistinguishability relations over histories (assuming perfect recall of agents). Then we use structural induction to prove that the truth of ATL formulae coincides in a model and its unfolding (the tricky part is to show that, for nested temporal subformulae, agents in the unfolding do not have more abilities despite having more precise knowledge). Thus, ioR-satisfiability in iCGS's implies ioR-satisfiability in tree unfoldings, but on tree unfoldings ioR and ior strategies coincide. ■

The converse does not hold:

Proof. To show this, we take the ATL embedding of the CTL duality between combinators E✷ and A✸. In fact, only one direction of the equivalence is important here:

First, we observe that: (i) ¬〈〈∅〉〉✸¬p expresses (regardless of the actual type of ability being considered) that there is a path in the system on which p always holds; (ii) in the "objective" semantics the set out(q, sAgt) always consists of exactly one path; (iii) for every path λ starting from q, there is an ioRstrategy sAgt such that out(q, sAgt) = {λ}. From these, it is easy to see that Φ4 is valid in ATLioR.

Second, we consider model M4 in Figure 4. 2 Let us take p ≡ ¬angry ∧ ¬suspicious. Then, we have M4, q0 |=ior ¬〈〈∅〉〉✸¬p but also M4, q0 ̸|=ior 〈〈Agt〉〉✷p, which demonstrates that Φ4 is not valid in ATLior. ■

Corollary 5 Val (ATLior) ⊊ Val (ATLioR).

2 The example depicts some simple traps that await a married man if he happens to be absent-minded. If he doesn't kiss his wife in the morning, he is likely to make her angry. However, if he kisses her more than once, she might get suspicious. It is easy to see that the absent-minded (i.e., memoryless) husband does not have a strategy to survive safely through the morning, though a "safe" path through the model does exist (λ = q0q1q1 . . . ).

Proposition 10 Val (ATLisr) ⊆ Val (ATLisR).

Proof idea. The proof is analogous to Proposition 8, but the unfolding is now a forest that takes into account trees that are subjectively possible from the agents' point of view (also in the subtrees - for nested strategic subformulae). ■

Finally, we consider the reverse direction.

Proposition 11 Val (ATLisR) ̸⊆ Val (ATLisr).

Proof. We takeΦ5

The formula states that if a has an opening move and a followup strategy to achieve p eventually, then these can be integrated into a single strategy achieving p already from the initial state. It is easy to see that Φ5 is valid in ATLisR, and that the single strategy is just a concatenation of the two strategies that we get on the left hand side of the implication. On the other hand, for the "poor duck model" M1 and p ≡ shot, we get that M1, q0 |=isr 〈〈a〉〉 ❣〈〈a〉〉✸p but also M1, q0 ̸|=isr 〈〈a〉〉✸p, so Φ5 is not valid in ATLisr. ■

Corollary 6 Val (ATLisr) ⊊ Val (ATLisR).

3.3 Between Subjective and Objective Ability

Finally, we compare validity sets for the semantic variants of ATL that differ on the outcome paths which are taken into account, i.e., whether only the paths representing the "objectively" possible courses of action are considered, or all the executions that are "subjectively" possible from the agents' perspective.

Proposition 12 Formula Φ2 ≡ 〈〈a〉〉✸p → p ∨ 〈〈a〉〉 ❣〈〈a〉〉✸p is valid in ATLioR and ATLior, but invalid in ATLisR and ATLisr.

Proof. We first prove validity of Φ2 in ATLior, which implies also validity in ATLioR by Proposition 8. Suppose that M, q |=ior 〈〈a〉〉✸p, then there must be an ir-strategy sA that enforces ✸p for every execution starting from q. But then, if p is not the case right at the beginning, sA must lead to a next state from which it enforces ✸p.

For the second part, invalidity of Φ2 in ATLisR was already proved in Proposition 5. Thus, by Proposition 10, Φ2 is not valid in ATLisr, too. ■

Proposition 13 Let us define an additional operator N ("now") as Nϕ ≡ ϕ U ϕ. Formula

is valid in ATLisR and ATLisr, but invalid in ATLioR and ATLior .

Proof. Analogously to Proposition 12, we will prove the validity of Φ6 in ATLisr, and its invalidity in ATLioR.

First, let M, q |=isr 〈〈a〉〉N〈〈c〉〉 ❣〈〈a〉〉 ❣p. Then, for every state q′ ∈ [q]∼a , c has an action αc that enforces 〈〈a〉〉 ❣p from [q′ ]∼c . By collecting these actions into an ir-strategy sc (we can do it since single actions are successful for whole indistinguishability classes of c), we have that sc enforces ❣〈〈a〉〉 ❣p from every state in [q]∼{a,c} , regardless of what the other players do (in particular, regardless of what a does). But then, for every execution λ of sc from [q]∼{a,c} , a will have a choice to enforce ❣p from λ[1]. Again, collecting these choices together yields an ir-strategy sa (we can fix the remaining choices arbitrarily). By taking s{a,c} = (sa, sc), we get a strategy for {a, c} that enforces that p will be true in two steps, from every state in [q]∼{a,c} . Hence, also M, q |=isr 〈〈a, c〉〉✸p.

For the invalidity, consider the "modified poor duck model" M2 augmented with additional agent c that has no choice (i.e., at each state, it has only a single irrelevant action wait available). Let us denote the new iCGS by M ′2 . If we identify p with shot, it is easy to see that M ′2 , q′0 |=ioR 〈〈c〉〉 ❣〈〈a〉〉 ❣p, and hence also M ′2 , q′0 |=ioR 〈〈a〉〉N〈〈c〉〉 ❣〈〈a〉〉 ❣p. On the other hand, M ′2 , q′0 ̸|=ioR 〈〈a, c〉〉✸p, which concludes the proof. ■

Corollary 7 For every y, z ∈ {R, r}, the sets Val(ATLisy) and Val (ATLioz) are incomparable.

4 Summary and Conclusions

In this paper, we compare validity sets for different semantic variants of alternating-time temporal logic. In other words, we compare the general properties of games induced by different notions of ability. It is clear that changing the notions of strategy and success in a game leads to a different game. The issue considered here is whether, given a class of games, such a change leads to a different class of games, too. And, if so, what is the precise relationship between the two classes.

A summary of the results is presented in Figure 5. The first, and most important, conclusion is that all the semantic variants discussed here are different on the level of general properties they induce; before our study, it was by no means obvious. Moreover, our results show a very strong pattern: perfect information is a special case of imperfect information, perfect recall games are special case of memoryless games, and properties of objective and subjective abilities of agents are incomparable.

Acknowledgements. Wojciech Jamroga acknowledges the support of the FNR (National Research Fund) Luxembourg under project S-GAMES - C08/IS/03. The authors would like to express their thanks to Jan Broersen for the argument that triggered this study, Valentin Goranko for discussions on (non-)validity of fixpoint properties in various semantics of ATL, and the anonymous reviewers for their remarks.