On Logics of Strategic Ability Based on Propositional Control

1 Introduction

Formal languages for reasoning about strategic behaviours of human and artificial agents have attracted much interest in recent years [Bulling et al., 2010; Goranko and Jamroga, 2004]. Typically, modal languages for temporal reasoning have been extended with operators to represent strategic abilities of coalitions [Alur et al., 2002; Chatterjee et al., 2010; Mogavero et al., 2014]. The resulting formalisms describe a rather abstract notion of agents' actions and strategies, which is appropriate for the various scenarios and use cases that have been successfully analysed within these frameworks [van der Hoek et al., 2006; ˇCerm´ak et al., 2014].

On the other hand, substantial effort has been put towards making strategic abilities more precise, by grounding formal semantics in computational theories of agency [Wooldridge, 2000]. In this direction, Coalition Logic of Propositional Control (CL-PC) [van der Hoek and Wooldridge, 2005; Gerbrandy, 2006; van der Hoek et al., 2010; 2011; Herzig et al., 2011] attempts to offer an explanation of the effectivity functions of Pauly's Coalition Logic [Pauly, 2002] in terms of the agents' control over propositional atoms. Basically, the models of CL-PC consist in a partition AP1↪ ▷ ▷ ▷ ↪APn of the set of propositional atoms, where each APi is the set of atoms whose truth value is controlled by agent i. Here the three key assumptions of Propositional Control (PC) are apparent: it is exhaustive (every atom is controlled by at least one agent), exclusive (every atom is controlled by at most one agent), and actions are unrestricted: any assignment of i's atoms is available to i in any state. It has been argued that Propositional Control is suitable for the specification and verification of rich multi-agent systems [van der Hoek et al., 2006; Troquard et al., 2011; Cin´a and Endriss, 2015; Herzig et al., 2016]. In particular, [van der Hoek and Wooldridge, 2005] shows that if we translate Pauly's coalition formulas ￿￿A￿￿X' - here written in the syntax of ATL, using the embedding of [Goranko, 2001] - into CL-PC formulas ◇A ￿Ag￿A ' then all principles of Coalition Logic are valid in CL-PC. However, CL-PC is strictly stronger than Coalition Logic: there are principles of the former that are not valid for the latter. This is mainly a consequence of the exclusiveness, exhaustiveness and unrestrictedness assumptions in CL-PC.

Our motivation for this paper is to provide a more finegrained theoretical analysis of Propositional Control in logics for strategies, particularly w.r.t. Alternating-time Temporal Logic (ATL). We start by defining a semantics for ATL based on the same notion of Propositional Control as in CLPC, namely, control is exclusive and exhaustive, and actions are unrestricted. These are strong hypotheses, which we will show to validate several counterintuitive principles. Thus, next we relax the exhaustiveness assumption in an attempt to move towards standard ATL. Ideally, our aim is to single out a PC-based class of Concurrent Game Structures (CGS) that has the same class of validities as standard ATL. This would mean that PC suffices as models for ATL: one might for example prove that an ATL formula is satisfiable by providing a PC-based CGS. Such a strong result is however unlikely as agents can interact in complex ways in CGS. Nonetheless, in this paper we take a first step towards this aim, by considering non-exhaustive PC with restricted actions. We analyse both semantics, including the model checking and satisfiability problems, and discuss differences w.r.t. standard ATL. Our results point out that unrestrictedness brings us immediately to the same complexity classes as full ATL.

Our paper is organized as follows. In Section 2 we present some preliminaries on CL-PC, ATL, and CGS. In Section 3 we introduce CGS-PC with unrestricted actions, and in Section 4 weak CGS-PC. For both classes we analyse the semantics and provide results for the model checking and satisfiability problems. We conclude by discussing some developments for future research. Proofs are often omitted for reasons of space, we only provide those we deem most significant.

2 Preliminaries

In this section we introduce the technical notions that will be used throughout the paper: CL-PC and CGS-based ATL. In the rest of the paper Ag = {1↪ ▷ ▷ ▷ ↪n} is the set of agents, and AP is the set of atomic propositions. Also, we denote the complement of a set U (w.r.t. some given set V ⊇ U) by U. Given a formula ', we define AP' as the set of atoms occurring in '. Furthermore, letting A ⊆ Ag be the set of agents occurring in ', we define Ag' as Ag if A = Ag, and as Ag ∪ {e} otherwise, for some e ∉ A. (The fresh agent e will mimic the set of agents not occurring in '.)

2.1 Coalition Logic of Propositional Control

The language of CL-PC is defined by the following BNF, for p ∈ AP and A ⊆ Ag: ' ∶∶= p ￿ ℜ' ￿ '→' ￿ ◇A' where ◇A reads "coalition A has the contingent ability to achieve ". The other propositional connectives and the box

operator ￿A, dual of ◇A, are defined as standard. Two semantics for CL-PC are provided in [van der Hoek and Wooldridge, 2005]: direct models and Kripke models. Since they are equivalent we here only present the former.

Definition 1 (Model). Given sets Ag of agents and AP of atoms, a model Μ is a partition AP1↪ ▷ ▷ ▷ ↪ AP￿Ag￿ of AP .

Every subset ✓ of AP can be identified with the valuation ✓ ∶ AP → {↵ ↪ tt} that assigns true tt to all atoms in ✓ and false ↵ to all atoms in ✓. We will use the two presentations interchangeably, without explicit mention.

Definition 2 (Semantics for CL-PC). We define whether model Μ satisfies formula ' according to valuation ✓, or (Μ↪ ✓) ￿ ', as follows (we omit the clauses for propositional connectives as straightforward):

where ✓ ⊕ ✓A = (✓ ∪ ✓A) ￿ (￿i∈A APi ￿ ✓A) is the update of ✓ according to ✓A.

A formula ' is true in a model Μ, or Μ ￿ ', iff (Μ↪ ✓) ￿ ' for all valuations ✓ ∈ 2AP ; ' is valid in a class Κ of models iff Μ ￿ ' for all Μ ∈ Κ. Notice that given Ag and a partition

AP1↪ ▷ ▷ ▷ ↪ AP￿Ag￿ of AP , there exists a unique model Μ. Models for CL-PC were originally defined on finite sets of atoms. Here we do not make such an assumption, as it is not normally considered in temporal logics. Moreover, by the following result, the two accounts are equivalent w.r.t. satisfaction of formulas.

Lemma 1. Given model Μ based on Ag, with partition AP1↪ ▷ ▷ ▷ ↪ AP￿Ag￿ of AP , valuation ✓, and formula ', we have that (Μ↪ ✓) ￿ ' iff (Μ'↪ ✓') ￿ ', where

• ✓' is the restriction of ✓ to AP'.
• Μ' is the model based on the set of agents Ag' and atoms AP', with partition AP1 ∩ AP'↪ ▷ ▷ ▷ ↪AP￿Ag′ ￿ ∩ AP' and, possibly, APe = ￿i∈Ag′ APi ∩ AP' (in case the fresh agent e is present);

We observed that, since coalition Logic corresponds to the X-fragment of ATL [Goranko, 2001], we can express the ATL formula ￿A￿X in CL-PC as ◇A ￿A . This remark prompts the question of interpreting ATL on CL-PC models. To do so, we introduce formally ATL and its semantics.

2.2 ATL and Concurrent Game Structures

• The semantics of ATL is in terms of a standard framework for the representation of games: Concurrent Game Structures. Definition 3 (CGS). Given sets Ag of agents and AP of atoms, a Concurrent Game Structure (CGS) is a tuple Γ = ￿S↪ Act↪ d↪ ⌧↪ ⇡￿ such that · S is a non-empty set of states;

Formulas in ATL are defined by the following BNF, for p ∈ AP and A ⊆ Ag: ' ∶∶= p ￿ ℜ' ￿ '→' ￿ ￿A￿X' ￿ ￿A￿G' ￿ ￿A￿'U' The formula ￿A￿X' reads "the agents in A have a strategy to enforce ' at the next state, no matter what the other agents do". Formulas ￿A￿G' and ￿A￿('U'′ ) read accordingly, where X stands for 'next' and U stands for 'until'.

• Act is a non-empty set of individual actions;

· ⌧ ∶ S ×Act￿Ag￿ → S is the transition function such that, for every s ∈ S and joint action ↵ ∈ Act￿Ag￿ , ⌧(s↪↵) is defined iff ↵i ∈ d(i↪ s) for every i ∈ Ag; · ⇡ ∶ S → 2AP is the state-labeling function. We remark that in Def. 3, states, actions, and the transition function are given as completely abstract notions: nothing is specified about the internal structure of states, about the nature of actions, nor about the computational properties of the transition function. Obviously, this responds to the need for a purely mathematical concept, proper of formal semantics. Nonetheless, we are interested in filling these abstract notions with some computational content, in order to give a computationally-grounded semantics to ATL [Wooldridge, 2000], specifically by using Propositional Control. But first we provide the interpretation of ATL on CGS. Hereafter we

• d ∶ Ag × S → (2Act ￿ {￿}) is the protocol function that returns the actions available to agents at each state;

write s ↵￿→ s′ whenever s′ = ⌧(s↪↵). Definition 4 (Strategy). Given a CGS Γ = ￿S↪ Act↪ d↪ ⌧↪ ⇡￿, a strategy for an agent i ∈ Ag is a function f ∶ S →Act that is compatible with d, i.e., for every s ∈ S, f(s) ∈ d(i↪ s).

A collective strategy for a coalition A is a set fA = {fi ￿ i ∈ A} of strategies. If fA is a collective strategy, s ∈ S, and ↵ ∈ Act￿Ag￿ , then ↵ ∈ ˆ fA(s) whenever (i) for i ∈ A, ↵i ∈ fi(s); and (ii) for i ∈ A, ↵i ∈ d(i↪ s). Further, the outcome out(s↪ fA) is the set of all infinite runs λ = s↪ s1↪ s2↪ ▷ ▷ ▷ such that for every j ￿ 0, for some ↵ ∈ ˆ fA(sj ), we have sj ↵￿→ sj+1. For a run λ and j ￿ 0, λ[j] denotes the j+1-th state sj .

Since the strategies in Def. 4 only take into account the present state of the system, they are called positional or memoryless [Bulling et al., 2010]. We recall that in contexts of perfect information, as the present one, semantically there is no difference between positional strategies and strategies with perfect recall. We work with the former for simplicity.

Definition 5 (Semantics for ATL). We define whether CGS Γ satisfies formula ' at state s, or (Γ↪ s) ￿ ', as follows (again we omit clauses for propositional connectives):

A formula ' is true in a CGS Γ, or Γ ￿ ', iff (Γ↪ s) ￿ ' for all states s ∈ S; ' is valid in a class Κ of CGS iff Γ ￿ ' for all CGS Γ ∈ K. We denote by Val (Κ) the set of ATL-validities in class Κ.

3 CGS with Propositional Control

We observed that the notion of CGS provided in Def. 3 is fairly abstract. For instance, the transition function ⌧ is unconstrained: given a state and an action, ⌧ can in principle return any state in S as a successor. In this section we introduce a notion of CGS that is based on Propositional Control. As customary in CL-PC, we assume that the set AP of atoms is partitioned into sets APi ⊆ AP, where i ∈ Ag. Further, for every P ⊆ AP, we consider atomic actions +P and -P, which respectively represent the action of setting the atoms in P to true and false.

We now introduce CGS with Propositional Control by providing concrete instances to the abstract elements in Def. 3.

Definition 6 (CGS-PC). A Concurrent Game Structure for Propositional Control is a CGS Γ = ￿S↪ Act↪ d↪ ⌧↪ ⇡￿ such that

• Act is the set of actions (+P↪-P ′ ), for disjoint P↪P ′ ⊆ AP ;
• S = 2AP1 × ▷ ▷ ▷ × 2AP￿Ag￿ , where each 2APi is the set of valuations ✓i ⊆ APi (which we identify with functions ✓i ∶ APi → {↵ ↪ tt}); 1
• protocol d satisfies: (+P↪ -P ′ ) ∈ d(i↪ s) iff P↪ P ′ ⊆ APi; · transition function ⌧ is such that, for every s ∈ S and ↵ ∈ Act￿Ag￿ , if s′ = ⌧(s↪↵), then each s′i is obtained by updating si according to ↵i = (+P↪-P ′ ), that is, s′i = (si ∪P) ￿P ′ ;

1 We could as well set S to 2AP , but prefer the current presentation in view of relaxing exhaustivity of control.

· function ⇡ is such that ⇡((s1↪ ▷ ▷ ▷ ↪ s￿Ag￿)) = ￿i∈Ag si. By Def. 6, the actions of each agent i are unrestricted: all and only actions involving atoms in APi are enabled for i. We require sets P and P ′ in action (+P↪-P ′ ) to be disjoint for ease of presentation (the restriction can be avoided by some mechanism resolving conflicting assignments.) We refer to +P (resp. -P ′ ) as the positive (resp. negative) effects of the action. In what follows we write actions +{p} and -{p}, for p ∈ AP, simply as +p and -p. As it is the case for CLPC, given sets Ag of agents and AP of atoms with partition AP1↪ ▷ ▷ ▷ ↪AP￿Ag￿, there is a unique CGS-PC built on Ag and AP. Notice also that the transition relation ￿→ such that s ￿→ s′ iff s ↵￿→ s′ for some joint ↵, is universal. Indeed, given states s and s′ , for every i ∈ Ag, consider action βi = (+(s′i ￿ si)↪ -(si ￿s′i )). Then, we have that (s′i ￿si) and (si ￿s′i ) are We now consider some formulas that are valid in CGS-PC but not in CGS, as well as the computational properties of the former. These provide interesting insights on the impact of the assumptions underlying Propositional Control in CGS, and the distance of the latter w.r.t. standard ATL.

disjoint, and s β￿→ s′ . Clearly, CGS-PC are a particular instance of CGS, that is, the class CGS-PC of all CGS-PC is a subclass of the class CGS of all CGS. In particular, the set Val(CGS) of validities in CGS is a subset of Val(CGS-PC). In the next section we will see that this inclusion is strict.

First, all ATL operators can be reduced to ￿A￿X. Lemma 2. The following formulas are valid in CGS-PC:

As a consequence of Lemma 2, we can think of the LHS of (1)-(3) as shorthands for the RHS. However, the expansion is exponential in the length of the original formula.

￿A￿G' ↔ '∧￿A￿X' (1) ￿A￿('U'′ ) ↔ '′ ∨ ('∧￿A￿X'′ ) (2) ￿A￿F' ↔ '∨￿A￿X' (3) Proof. We prove (1). The '→' direction holds in standard CGS. As to the '←' direction, suppose (Γ↪ s) ￿ ' ∧ ￿A￿X', that is, (Γ↪ s) ￿ ' and for some action tuple ↵A, for all action tuples ↵A, s ↵A⋅↵A ￿￿￿￿→ s′ implies (Γ↪ s′ ) ￿ '. Now consider action tuple ↵′A s.t. ↵′i = (+￿↪-￿) for every i ∈ A, and any action tuple ↵′A. If s′ ↵′A⋅↵′A ￿￿￿￿→ s′′ then also s ↵A⋅↵′′A ￿￿￿￿→ s′′ by considering action ↵′′ i = (+(s′′ i ￿ si)↪-(si ￿ s′′ i )) for every i ∈ A. But then (Γ↪ s′′ ) ￿ ' by hypothesis. By reasoning along this way, we find a strategy fA ("first ensure ' and then do nothing") such that for every λ ∈ out(s↪ fA) and j ￿ 0, (Γ↪ λ[j]) ￿ '. The proofs for (2) and (3) are similar.

The next equivalences follow from Lemma 2 and the universality of the transition relation ￿→.

Lemma 3. The following formulas are valid in CGS-PC: ￿A￿X' ↔ ('∧￿A￿G') ∨ (ℜ'∧￿A￿F') ￿A￿X' ↔ ￿A￿X￿A￿X' Hereafter we consider some interesting consequences of the exclusiveness and exhaustiveness of Propositional Control, as formulated for atomic propositions, where ˙￿i∈A' abbreviates ￿i∈A(' ∧ ￿j∈A↪j≠i ℜ'[j￿i]) and where '[j￿i] results from uniformly replacing all occurrences of i in ' by j.

Proof. As regards (4), the '←' direction is standard in CGS. As to the '→' direction, suppose that (Γ↪ s) ￿ ￿A￿X(p ∨ q). This means that for some action tuple ↵A, for all action tuples ↵A, s ↵A⋅↵A ￿￿￿￿→ s′ implies (Γ↪ s′ ) ￿ p ∨ q. If (Γ↪ s′ ) ￿ p, then for some i ∈ A, p ∈ APi, and therefore (Γ↪ s) ￿ ￿i￿Xp. By coalition monotonicity we obtain (Γ↪ s) ￿ ￿A￿Xp, and finally (Γ↪ s) ￿ ￿A￿Xp ∨ ￿A￿Xq. The case (Γ↪ s′ ) ￿ q is analogous. The proof of (5) is similar; whereas formulas (6) and (7) are valid because control is exhaustive.

Intuitively, (4) and (5) entail that a coalition A controls a non-tautological disjunction (resp. satisfiable conjunction) of atoms iff A controls each disjunct (resp. conjunct). Also, by (6) and (7) a coalition A controls an atom p iff p is controlled by exactly one member of A.

The following validities also illustrate the role of exclusiveness and exhaustiveness of control in CGS-PC.

Lemma 5. The following formulas are valid on CGS-PC:

Observe that the above principles (1)-(11) are sometimes too restrictive. Consider 4: it may be the case that I can throw a coin on a chessboard without being able to throw it on a white filed or a black field.

Using the above lemmas, we now prove the following result on the relationship between CL-PC and the Concurrent Game Structures for Propositional Control. Recall that in CL-PC, ￿A￿X' is a shorthand for ◇A￿A '. Moreover, abusing notation a bit, we consider ￿A￿G-, ￿A￿F-, and ￿A￿Uformulas as shorthands according to (1)-(3).

Proof. '⇐': Suppose CL-PC ￿￿ ', that is, for some model Μ and valuation ✓ of AP, (Μ↪ ✓) ￿￿ '. Then, consider the (unique) CGS-PC Γ defined on the same Ag and the same partition of AP as Μ. We now prove that for every ATL formula , (Μ↪ ✓) ￿ iff (Γ↪ ✓) ￿ , by induction on . For = p, (Μ↪ ✓) ￿ iff p ∈ ✓, iff (Γ↪ ✓) ￿ . The inductive cases for propositional connectives are straightforward. As for ATL operators, if (Μ↪ ✓) ￿ ￿A￿X ′ , then for some Avaluation ✓A, for everyA-valuation ✓A, (Μ↪ (s⊕✓A)⊕✓A) ￿ ′ . But this means that for some A-action ✓A, for every Aaction ✓A, ✓ ✓A⋅✓A ￿￿￿→ ✓′ implies (Γ↪ ✓′ ) ￿ ′ by induction hypothesis, i.e., (Γ↪ ✓) ￿ ￿A￿X ′ . As a result, (Γ↪ ✓) ￿￿ ', and therefore ' is not a validity in CGS-PC either.

Theorem 6. For every ATL formula ', CL-PC ￿ ' iff CGS-PC ￿ '.

We omit the '⇒'-direction, which is proved similarly.

By Theorem 6, CGS-PC is indeed the class of CGS that correspond to CL-PC w.r.t. the language of ATL, as the two frameworks share the same set of validities. Note that Theorem 6 does not provide a complexity result, given that the expansion of abbreviations may result in exponential growth.

As anticipated in the introduction, our aim is to analyse the computational properties of ATL interpreted on CGS-PC. Specifically, we are interested in the following problems:

• Satisfiability: given a formula ', determine whether ' is satisfied in some model.
• Model checking: given a CGS-PC Γ, a state s, and a formula ', determine whether (Γ↪ s) ￿ '.

As an auxiliary step to study these problems, consider the following corollary of Theorem 6 and Lemma 1.

Corollary 7. Given CGS-PC Γ based on Ag, with partition AP1↪ ▷ ▷ ▷ ↪ AP￿Ag￿ of AP , state s, and formula ', we have that (Γ↪ s) ￿ ' iff (Γ'↪ s') ￿ ', where

• s' is the restriction of s to AP'.
• Γ' is the CGS-PC based on sets AP' and Ag' as defined in Lemma 1;

By Corollary 7, the size of the input for the model checking problem can be given as ￿Γ'￿ + ￿'￿, where the size ￿Γ'￿ = ￿Ag'￿+￿AP'￿ of Γ' is polynomial in '; whereas satisfiability can be restricted to CGS-PC built on Ag' and AP'.

We are now able to prove the following.

Theorem 8. Both the model checking problem and the satisfiability problem for CGS-PC are ∆P3 -complete.

Proof. As regards model checking, we follow [Bulling et al., 2010]. For the lower bound we make use of QSAT2, a ⌃P2 -complete problem, as an intermediate step. Specifically, given an instance ∃p1↪ ▷ ▷ ▷ ↪ pr∀pr+1↪ ▷ ▷ ▷ ↪ pk' of QSAT2, for boolean ' built on atoms p1↪ ▷ ▷ ▷ ↪ pk, we consider the CGSPC Γ defined on Ag = {1↪ 2} s.t. AP1 = {p1↪ ▷ ▷ ▷ ↪ pr} and AP2 = {pr+1↪ ▷ ▷ ▷ ↪ pk}. Then, QSAT2 is reduced to model checking ￿1￿X'. Finally, to obtain ∆P3 -hardness, ￿1￿X' is combined with nested cooperation modalities, so as to reduce the SNSAT3 problem along the lines of [Laroussinie et al., 2008].

As to the upper bound, we outline the following procedure for checking (M↪ s) ￿ ￿A￿X' with no nested modalities. First, we guess an action tuple ↵A. Then, we check if the CTL formula AX' is true in state s of the resulting model by asking an oracle for counteractions ↵A to make X' false, and then we revert the oracle's reply. Nested ATL modalities can be dealt with in polynomial time.

As regards satisfiability, notice that we can check whether a formula ' is satisfiable by model checking it on the CGS-PC Γ', as defined in Corollary 7. Hence, the problem is in ∆P3 . As to hardness, we can reduce SNSAT3 to CGS-PC satisfiability similarly to what done above for the model checking problem.

As a consequence of Theorem 8, model checking CGS-PC has exactly the same complexity as the implict model checking problem for ATL [Bulling et al., 2010]. On the other hand, satisfiability for standard ATL is EXPTIME-complete. So the assumptions underlying PC have a noticeable computational impact on satisfiability. Observe that our complexity results differ from those for CL-PC, where both model checking and satisfiability are PSPACE complete [van der Hoek and Wooldridge, 2005].

4 Weakening CGS-PC

In Section 3 we introduced the class of CGS-PC, which we proved to have the same set of validities as CL-PC. However, we may consider some of these validities (e.g., those in Lemma 2) as being too strong and look for a more ATL-like semantics. Ideally, one would like to define a class Κ of CGS for Propositional Control such that Val(Κ) = Val(CGS). We discussed the limitation of such an endeavour when it comes to interaction between agents. Nonetheless, in this section we move a step towards standard CGS by dropping the assumptions of exhaustiveness and unrestricted actions. Specifically, we introduce the notion of weak CGS-PC, or CGS-PC- .

• S, Act, ⌧ , ⇡ are defined as for CGS-PC;

Definition 7 (CGS-PC- ). A weak Concurrent Game Structure for Propositional Control is a CGS Γ = ￿S↪Act↪ d↪ ⌧↪ ⇡￿ such that

• the protocol d satisfies: (+P↪-P ′ ) ∈ d(i↪ s) only if

Clearly, CGS-PC are particular instances of CGS-PC- , which in turn are instances of CGS. In particular, we have the following strict inclusions:

P↪P ′ ⊆ APi; By Def. 7 the difference between CGS-PC- and CGS is that control is no longer exhaustive and protocol d no longer allows for changing any atom at any state. We will see that these small changes have a noticeable impact on validities. First of all, since an agent a might have only a subset of the set of actions (+P↪-P ′ ) with P ∪ P ′ ⊆ APa available at a state s, the transition relation ￿→ between states is neither reflexive, nor symmetric, nor transitive. (For example, reflexivity fails in a CGS-PC as soon as there is an agent without the empty action (￿↪￿) in her repertoire.) So it is not a universal relation. This contrasts with the situation for CGS-PC in Section 3.

(Γ↪ s0) ￿￿ ￿a￿X(q ∧ r). As to (4), consider the CGS-PC- Γ = ￿S↪Act↪ d↪ ⌧↪ ⇡￿, defined on set Ag = {a↪ b} of agents, s.t. for every s ∈ S, d(a↪ s) = {(+pa↪-￿) ￿ pa ∈ APa}; while d(b↪ s) = {(+pb↪-￿)↪ (+p′b ↪-￿)}, that is, agent b can (and must) set the value of exactly one of atoms pb↪ p′b to true in any state. Consider state s0 = ￿✓a↪ ✓b￿ for ✓a = ✓b = ￿. Clearly, (Γ↪ s0) ￿ ￿a￿X(pb ∨ p′b ). However, (Γ↪ s0) ￿￿ ￿a￿Xpb and

Proof. We provide counterexample CGS-PC- for (3) and (4). As to (3), consider the CGS-PC- Γ = ￿S↪Act↪ d↪ ⌧↪ ⇡￿, defined on set Ag = {a} of agents, s.t. for every s ∈ S, d(a↪ s) = {(+p↪-￿) ￿ p ∈ APa}, that is, agent a can only set the value of exactly one atom to true in any state. Consider now state s0 = ￿✓a￿ for ✓a = ￿. Clearly, for q↪ r ∈ APa, (Γ↪ s0) ￿ ￿a￿F(q ∧ r). However, (Γ↪ s0) ￿￿ q ∧ r and

(Γ↪ s0) ￿￿ ￿a￿Xp′b . As to (6) and (7), suppose none of the agents has an action making p true in his repertoire: then ￿A￿Xp is true for every A, i.e., the negative condition in ˙￿i∈A￿i￿Xp fails.

Generally speaking, (1)-(11) all fail due to restrictions on enabled actions.

The fact that control is exclusive (for all i↪ j ∈ Ag, APi ∩ APj = ￿), that the actions available to agent i may involve only a proper subset of 'her' actions on APi, and that control is constant in time makes that only a weakened version of (11) is valid.

Proof. Let i be the agent s.t. p ∈ APi, if any; any agent in Ag, otherwise. In the latter case, if (Γ↪ s) ￿ ￿Ag￿Xp then for some s′ ∈ Γ, s → s′ and (Γ↪ s′ ) ￿ p. But the truth value of p has not changed in the transition from s to s′ , that is, (Γ↪ s) ￿ p. Since no agent can affect the truth value of p, (Γ↪ s) ￿ ￿i￿Xp. On the other hand, if p ∈ APi for some i ∈ Ag, then we have two subcases to consider. If action +p is not enabled in state s, then once again the value of p does not changed from s to s′ , that is, (Γ↪ s) ￿ p and also (Γ↪ s) ￿ ￿i￿Xp. If +p does appear in some action available to i in s, then (Γ↪ s) ￿ ￿i￿Xp by setting the value of p to true. The proof for (Γ↪ s) ￿ ￿Ag￿Xℜp is similar.

(Γ(3)↪ s(3)) ￿ (3), as (3) is valid in the class of CGS-PC. For CGS-PC- we have the following result, according to a different notion of restriction Γ'.

On the other hand, Cor. 7 does not hold for CGS-PC- . First of all, notice that, given a CGS-PC- , Γ' as defined in Cor. 7 is a CGS-PC. Therefore, if Γ is the first CGS-PC- in the proof of Lemma 9, we have that (Γ↪ s) ￿￿ (3). However,

Lemma 11. Given a CGS-PC- Γ based on Ag and AP1↪ ▷ ▷ ▷ ↪AP￿Ag￿, state s, and formula ', we have that (Γ↪ s) ￿ ' iff (Γ'↪ s') ￿ ', where

• Γ' = ￿S'↪Act'↪ d'↪ ⌧'↪ ⇡'￿ is the CGS-PC- based on set Ag' of agents defined as in Lemma 1, and on set AP' ∪ S of all atoms appearing in ' together with the states in Γ as new atoms, with AP ′ i = APi ∩ AP' for every i ∈ Ag', and APe = S. Moreover, ↵ ∈ d(i↪ s) iff the restriction ↵￿AP′ i belongs to d'(i↪ s′ ) for s′e = s and i ∈ Ag, and ↵ ∈ d(e↪ s′ ) iff ↵ = (-s′e ↪+t), where t is a successor of s′e in Γ. · s' is the tuple (✓1 ∩AP'↪ ▷ ▷ ▷ ↪ ✓Ag' ∩AP'↪ s). Notice that the restriction Γ' for CGS-PC- is an infinite state systems in general, differently from the case for CL-PC and CGS-PC.

We can now consider the model checking and satisfiability problems for CGS-PC- .

1. The satisfiability problem for CGS-PC - is EXPTIMEhard.

Theorem 12. 1. The model checking problem for CGS-PC - is ∆P3 -complete.

Proof. As to model checking, the result follows from the corresponding result for CGS-PC. Specifically, the lower bound follows by remarking that the CGS-PC used in the reduction of SNSAT3 in Theorem 8 is a CGS-PC- trivially. The upper bound follows from the result available for implicit model checking of ATL w.r.t. CGS [Bulling et al., 2010].

As to satisfiability, we follow [van der Hoek et al., 2006] and reduce the problem of deciding whether a given agent has a winning strategy in the two-player game PEEK-G4 [Stockmeyer and Wong, 1979]. An instance of PEEK-G4 consists in a quadruple (X0↪ X1↪ X2↪Win) where X0, X1 and X2 are finite sets of propositional variables such that X0 ⊆ X1 ∪X2, X1 and X2 are disjoint, and Win is a propositional formula over X1∪X2. The idea is that X0 is the initial valuation and that X1 and X2 are variables that are respectively under the control of agent 1 and 2. At X0, 1 starts by selecting a variable in X1 and assigning it to either true or false (possibly leaving it unchanged); then 2 selects a variable in X2 and assigns it; and so on. An agent wins if his move makes the winning condition ' true. The problem is to decide whether 2 has a winning strategy in a given instance (X0↪X1↪X2↪Win) of the game. Given (X0↪X1↪X2↪Win), consider the following formulas describing it in the language of ATL:

Formula '0 characterizes the initial state, where t1 expresses that it is agent 1's turn. '1 says that the agents play in turns. '2 says that at her turn, 1 can assign each of her variables at will, while '3 says that at that turn, 2 cannot modify any of her variables. '4 and '5 say the same thing for 2. '6 says that at each turn at most one variable can change truth value. Player 2 has a strategy guaranteeing Win if and only if

('0 ∧ '2 ∧ '3 ∧ '4 ∧ '5 ∧ '6) → ￿￿2￿￿FWin is valid in CGS-PC- . Moreover, the length of '0 ∧￿∧'6 is quadratic in the cardinality of X1 ∪X2.

We conjecture that EXPTIME membership of the satisfiability problem for CGS-PC - can be shown by proving that ' is satisfiable in CGS-PC - iff '∧ is satisfiable in CGS, where formula is of length polynomial in the length of ' and characterizes CGS-PC - . Such a formula should characterize that control is exclusive and constant: we conjecture that is the formula (12) of Lemma 10.

5 Conclusion

In this paper we took the first steps to fill the gap between ATL and CL-PC by introducing two classes of CGS that are based on Propositional Control. The first class CGS-PC consists in a single structure (modulo agents and partition of atoms) that can be represented in a compact way, and whose complexity is the same as CL-PC. The second CGS-PC - is a family of structures, depending on the restriction of action availability at each state, whose computational properties closely resemble those of standard ATL.

Related Literature. Recent years have witnessed a growing interest in various forms of Propositional Control, possibly combined with dynamic and epistemic aspects [van der Hoek et al., 2011; Balbiani et al., 2013; 2014]. It is beyond the scope of this paper to provide an exhaustive account. We focus on [van der Hoek et al., 2006], which is closest to our contribution. The approach of this work is based on Simple Reactive Modules (SML), which are basically agents whose propositional control is described by rules of the form ' ￿ (+P↪ -P ′ ), where ' is a boolean condition and (+P↪ -P ′ ) is an action. In this respect SML can be seen as a class strictly included between CGS-PC and weak CGS-PC, different from both. Also, while our motivation is mainly theoretical, the focus in [van der Hoek et al., 2006] is on the verification of multi-agent systems.

Future Work. There are a many interesting extensions of the present framework for future work. A low-hanging fruit is to add control changing actions to CGS, as done in [van der Hoek et al., 2010]. One of the consequences, for instance, is that formula (12) has to be weakened by dropping the temporal quantifier ￿￿￿￿￿G. Another interesting research direction is to lift the exclusiveness assumption and allow for multiple agents to control the same atom. The value of the atom at the next state can then be determined by a boolean function taking into account all choices of agents. We anticipate to consider various classes of boolean functions, representing interesting notions in game theory and social choice theory, in the spirit of [Grandi and Endriss, 2013]. Finally, we plan to extend our approach by an epistemic dimension, taking inspiration from recent approaches that are based on the concept of Propositional Visibility [van der Hoek et al., 2011; van Benthem et al., 2015; Herzig et al., 2015; Charrier et al., 2016], where an agent might observe or not the value of a propositional atom. Just as CGS can be built from Propositional Control, models of epistemic logic can be built from Propositional Visibility; and similarly to PC models, they can be represented in a compact way.

Acknowledgements. Thanks are due to the AAMAS reviewers whose comments helped us to improve the paper.