The Ceteris Paribus Structure of Logics of Game Forms (Extended Abstract)

1 Introduction

The logical analysis of agency and games-for an expository introduction to the field see van der Hoek and Pauly's overview paper 2007-has boomed in the last two decades giving rise to a plethora of different logics in particular within the multi-agent systems field. 1 At the heart of these logics are always representations of the possible choices (or actions) of groups of players (or agents) and their powers to force specific outcomes of the game. Some logics take the former as primitives, like STIT (the logic of seeing to it that, [Belnap et al., 2001; Horty, 2001]), some take the latter like CL (coalition logic, [Pauly, 2002; Goranko et al., 2013]) and ATL (alternating-time temporal logic, [Alur et al., 2002]).

In these formalisms the power of players is modeled in terms of the notion of effectivity. In a strategic game, the α-effectivity of a group of players consists of those sets of outcomes of the game for which the players have some collective action which forces the outcome of the game to end up in that set, no matter what the other players do [Moulin and Peleg, 1982]. So, if a set of outcomes X belongs to the α-effectivity of a set of players J, there exists an individual action for each agent in J such that, for all actions of the other players, the outcome of the game will be contained in X. If we keep the actions of the other agents fixed, then the selection of an individual action for each agent in J corresponds to a choice of J under the assumption that the other agents stick to their choices.

Scientific Context It was already observed by [van Benthem et al., 2009] that this formalization of choice and power Franc¸ois Schwarzentruber ENS Rennes francois.schwarzentruber@ens-rennes.fr in games is of an 'all other things being equal', or ceteris paribus, nature. Considering which outcomes of a game are possible for a set of players J once the other players have fixed their actions, amounts to considering what may be the case under the ceteris paribus condition 'all actions of the agents not in J being equal (to their current ones)'. In the current paper we leverage this intuition further and show how it can provide a novel systematization of many of the most influential formalisms in the field of logic and games.

∗The full version of this paper is published as The Ceteris Paribus Structure in Logics of Game Forms, Journal of Artificial Intelligence Research, volume 53 (2015) pp. 91-126.

1 The richness of this logical landscape was the object of the IJCAI'13 invited talk by A. Herzig Logics for Multi-Agent Systems: a Critical Overview.

Formal relationships linking the logics (or fragments thereof) we mentioned above have been object of several publications. Notable examples are: the embedding of CL into the next-time fragment of ATL [Goranko, 2001] and the embedding of CL into NCL (normal coalition logic, [Broersen et al., 2007; Balbiani et al., 2008a]), the embedding of CL and ATL into STIT [Broersen et al., 2005; 2006]. Earlier contributions have also attempted more comprehensive systematizations of the field of logic and games. Two in particular are worth mentioning: Goranko and Jamroga's work 2004, which compares game logics based on the computation tree abstraction like ATL and its variants; and Herzig's work 2014, which provides a conceptual and syntaxbased-while we favor here semantic methods-comparison of all the main formalisms in the literature.

We focus on the components of the semantics of those logics that have directly to do with the representation of choice and power, and we abstract away from the representation of time and repeated interaction. So the logics we will be working with are: the atemporal fragment of STIT, logic CL-PC (coalition logic of propositional control, [van der Hoek and Wooldridge, 2005]) and the starless fragment of DL-PA (dynamic logic of propositional assignments, [van Eijck, 2000; Balbiani et al., 2013]). These logics cover, arguably, a large spectrum of the most influential existing formalisms. Logic STIT is often considered a standard in the literature, as it embeds both CL and ATL [Broersen et al., 2005; 2006], so we use it as a natural starting point. Logic CL-PC is an influential extension of CL. Finally, logic DL-PA is an extension of PDL (propositional dynamic logic, [Harel et al., 2000]), recently proposed in [Herzig et al., 2011; Balbiani et al., 2013].

Contribution To articulate our analysis, whose main technical tool consists of satisfiability-preserving embeddings, the paper introduces and studies-in its axiomatization and complexity-a simple ceteris paribus logic based on propositional equivalence, which we call CP. Such logic is the yardstick allowing us to compare and unify STIT, CL-PC and DL-PA. Figure 1 gives a graphical presentation of the embeddings established in the paper-as well as relevant ones already known in the literature.

An arrow indicates that each formula of the source logic is satisfiable if and only if a suitable translation of that formula is satisfiable in the target logic. DL-PA denotes the starless version of dynamic logic of propositional assignments, NCL and STIT denote the atemporal version of, respectively, normal coalition logic and the seeing-to-it logic. S5 denotes the normal modal logic of equivalence relations. Dotted lines indicate embeddings known in the literature: from CL-PC to DL-PA [Balbiani et al., 2013] and from STIT to NCL (and vice versa) with respect to fragments of the respective languages [Lorini and Schwarzentruber, 2011]. The embedding from STIT to CP assumes a bound on the STIT-models. All embeddings are polynomial except for the one from CP to S5.

2 A Simple Ceteris Paribus Logic

2.1 Equivalence Modulo a Set of Atoms

Consider a structure (W, V ) where W is a set of states, and V : P -→ 2W a valuation function from a countable set of atomic propositions P to subsets of W.

Definition 1. (Equivalence modulo X) Given a pair (W, V ), X ⊆ P and |X| < ω, the relation ∼VX ⊆ W 2 is defined as:

WhenX is a singleton (e.g. p), we will oftenwrite∼Vp instead of ∼V{p} . Also, in order to avoid clutter, we will often drop the reference to V in ∼VX when clear from the context.

Intuitively, two states w and w′ are equivalent up to set X, or X-equivalent, if and only if they satisfy the same atoms in X (according to a given valuation V ). The finiteness of X is clearly not essential in the definition. It is assumed because, as we will see, each set X will be taken to model a set of actions of some agent in a game form and sets of actions are always assumed to be finite.

Fact 1. (Properties of ∼X) The following holds for any set of states W, valuation V : P -→ 2W and finite sets X, Y ⊆ P:

(i) ∼X is reflexive, transitive and symmetric; (ii) if X ⊆ Y then ∼Y ⊆ ∼X; (iii) if X is a singleton, ∼X induces a partition of W with at most 2 cells; (iv) ∼X ∩ ∼Y = ∼X∪Y ; (v) ∼∅ = W 2 .

2.2 AModal Logic of the ∼X Relation

In this section we consider a simple modal language interpreted on relations ∼X and axiomatize its logic on the class of structures (W, V ). The key modal operator of the language will be 〈X〉, whose intuitive meaning is 'ϕ is the case in some state which is X-equivalent to the current one' or, to stress a ceteris paribus reading, 'ϕ is possible all things expressed in X being equal'. We call the resulting logic propositional ceteris paribus logic, CP in short.

Let P be a countable set of atomic propositions. The language LCP(P) is defined by the following BNF:

where p ranges over P and X is a finite subset of atomic propositions (X ⊆ P and X finite). Note that as the set of finite subsets of atomic propositions is countable, the language LCP(P) is also countable. The Boolean connectives ⊤, ∨,→,↔ and the dual operators [X] are defined as usual. Although we have taken diamond operators as primitive, we will for convenience also make use of box operators to state some results in later sections. The set SF(ϕ) of subformulas of a formula ϕ is defined inductively in the usual way.

This is the class of models we will be working with:

Definition 2. (CP-models) Given a countable set P, a CPmodel for LCP(P) is a tuple M = (W, V ) where: W is a non-empty set of states; V : P -→ 2W is a valuation function. A CP-model is called universal if W = 2P and V is s.t. V (p) = {w | p ∈ w}. It is called non-redundant if ∼P is the identity relation in W 2 .

Intuitively, a CP-model consists just of a state-space and a valuation function for a given set of atoms.

Definition 3. (Satisfaction for CP-models) LetM= (W, V ) be an CP-model for LCP(P), w ∈ W and ϕ, ψ ∈ LCP(P) (Boolean clauses omitted):

Formula ϕ is CP-satisfiable, if and only if there exists a model M and a state w such that M,w |=CP ϕ. Formula ϕ is valid inM, notedM |=CP ϕ, if and only if for all w ∈ W, M, w |=CP ϕ. Validity and consequence are defined as usual.

So, modal operators are interpreted on the equivalence relations ∼X induced by the valuation of the model. It is worth observing that the logic of this class of models is not closed under uniform substitution, 2 that is, logic CP is not uniform. 3 To witness that, notice that formula [{p}]p∨ [{p}]¬p is valid, whereas [{p}]ϕ ∨ [{p}]¬ϕ is not.

2 For the definition of uniform substitution the reader is referred to the textbook by [Blackburn et al., 2001, Def. 1.18].

3 The terminology comes from Goldblatt's work 1992.

Lemma 1. Let L∅CP (P) the set of formulae ϕ ∈ LCP(P) containing only 〈∅〉 operators. The set of formulae of L∅CP (P) which are CP-valid is the modal logic of Kripke frames (W,W 2 ), i.e., logic S5.

In other words, the 〈∅〉 operator of LCP is nothing but the global modality [Blackburn et al., 2001, pp. 367-370]. The next lemma states that CP is actually the logic of the class of relevant CP-models.

Lemma 2. Every satisfiable CP-formula is satisfiable on a non-redundant model.

One can obtain a sound and strongly complete axiom system for CP by a standard reduction technique exploiting Lemma 1. It can also be shown that CP can be embedded in S5 by an exponential satisfiability-preserving translation, and therefore that the satisfiability problem for CP is decidable and in NEXPTIME. We refer to the full paper for the details.

3 The Ceteris Paribus Structure of STIT

3.1 Atemporal Group STIT

First let us recall the syntax and the semantics of atemporal group STIT. The language of this logic is built from a countable set of atomic propositions P and a finite set of agents AGT = {1, . . . , n} and is defined by the following BNF:

where p ranges over P and J ranges over 2AGT . The construction [J : stit]ϕ is read "group J sees to it that ϕ is true regardless of what the other agents choose". We define the dual operator 〈J : stit〉ϕ def = ¬[J : stit]¬ϕ. When J = ∅, the construction [∅ : stit]ϕ is read "ϕ is true regardless of what every agent chooses" or simply "ϕ is necessarily true".

Definition 4 (STIT-Kripke model, [Herzig and Schwarzentruber, 2008]). A STIT-Kripke model M = (W, {RJ }J⊆AGT , V ) is a 3-tuple where:

• W is a non-empty set of worlds;
• for all J ⊆ AGT, RJ is an equivalence relation such that: (i) RJ ⊆ R∅; (ii) RJ = ⋂j∈J R{j}; (iii) for all w ∈ W and (w1, . . . ,wn) ∈ W n , if u1 ∈ R{1}(w), . . . , un ∈ R{n}(w) then ⋂1≤j≤n R{j}(uj) ̸= ∅;
• V : P → 2W is a valuation function for atomic propositions;

The partition induced by the equivalence relation RJ is the set of possible choices of the group J. Indeed, in STIT a choice of a group J at a given world w is identified with the set of possible worlds RJ(w). We call RJ(w) the set of possible outcomes of group J's choice at world w, in the sense that group J's current choice at w forces the possible worlds to be in RJ(w). The set R∅(w) is simply the set of possible outcomes at w, or said differently, the set of outcomes of the current game at w. According to Condition (i), the set of possible outcomes of a group J's choice is a subset of the set of possible outcomes. Condition (ii), called additivity, means that the choices of the agents in a group J is made up of the choices of each individual agent and no more. Condition (iii) corresponds to the property of independence of agents: whatever each agent decides to do, the set of outcomes corresponding to the joint action of all agents is nonempty. More intuitively, this means that agents can never be deprived of choices due to the choices made by other agents. In Lorini and Schwarzentruber's work 2011 determinism for the group AGT was assumed. That is to say that the set of outcomes corresponding to a joint action of all agents is a singleton. Horty's group STIT logic [Horty, 2001] does not suppose this. Here we deal with Horty's version of STIT. So a STIT model is a game form in which a joint action of all agents might determine more than one outcome.

3.2 Embedding Atemporal STIT into CP

That STIT is not embeddable into CPcan be inferred from various reasons, for instance: STIT satisfiability problem is undecidable if there are more than 3 agents [Herzig and Schwarzentruber, 2008], unlike CP; STIT does not have the finite model property [Herzig and Schwarzentruber, 2008], unlike CP, which we have seen is embeddable S5.

We can nevertheless embed a variant of group STIT under the assumption that every agent has a finite and bounded number of actions in his repertoire. The embedding uses a special formula GRIDm which enforces a CP model to encode a game form, and a suitably defined translation tr1.

Theorem 1. Let us consider a group STIT formula ϕ. Let m be an integer. Then the following items are equivalent: 1. ϕ is STIT-satisfiable in a STIT-model where each agent has at most 2m actions; 2. ϕ is STIT-satisfiable in a STIT-model where each agent has exactly 2m actions; 3. GRIDm ∧ tr1(ϕ) is CP-satisfiable.

3.3 Atemporal Individual STIT

In this subsection, we consider the following fragment of STIT called atemporal individual STIT:

LI-STIT(P,AGT) : ϕ ::= p | ¬ϕ | (ϕ∧ϕ) | [{j} : stit]ϕ where p ranges over P and j ranges over AGT .

This fragment of STIT, axiomatized by [Xu, 1998], has the exponential finite model property (see Lemma 7 in [Balbiani et al., 2008b]). Moreover, as the following theorem highlights, it can be embedded in logic CP, through the above translation.

Theorem 2. Let us consider a STIT formula ϕ of the individual STIT fragment. Let m be the length of ϕ. Then the following three items are equivalent: 1. ϕ is STIT-satisfiable 2. ϕ is STIT-satisfiable in a model where each agent has at most 2m actions; 3. GRIDm ∧ tr1(ϕ) is CP-satisfiable.

Thanks to Theorem 2, we reduce the NEXPTIMEcomplete satisfiability problem of individual STIT [Balbiani et al., 2008b] to the CP-satisfiability problem. As the reduction is polynomial, we obtain the following lower bound complexity result for the CP-satisfiability problem. We thus obtain also a lower bound result of NEXPTIME-hardness for the complexity of the satisfiability problem of CP.

4 The Ceteris Paribus Structure of Coalition Logic of Propositional Control

4.1 Logic CL-PC

CL-PC was introduced by [van der Hoek and Wooldridge, 2005] as a formal language for reasoning about capabilities of agents and coalitions in multiagent environments. In this logic the notion of capability is modeled by means of the concept of control. In particular, it is assumed that each agent i is associated with a specific finite subset Pi of the finite set of all propositions P. Pi is the set of propositions controlled by the agent i. That is, the agent i has the ability to assign a (truth) value to each proposition Pi but cannot affect the truth values of the propositions in P\Pi. In the variant of CL-PC studied by [van der Hoek and Wooldridge, 2005] it is also assumed that control over propositions is exclusive, that is, two agents cannot control the same proposition. Moreover, it is assumed that control over propositions is complete, that is, every proposition is controlled by at least one agent.

The language of CL-PC is built from a finite set of atomic propositions P and a finite set of agents AGT = {1, . . . , n}, and is defined by the following BNF:

where p ranges over P and J ranges over 2AGT . Operator ♦J is called cooperation modality, and the construction ♦Jϕ means that "group J has the contigent ability to achieve ϕ".

Definition 5 (CL-PC model). A model for CL-PC is a tuple M= (P1, . . . ,Pn,X) where: (i) P1, . . . ,Pn is a partition of P among the agents in AGT; (ii) X ⊆ P is the set of propositions which are true in the initial state.

For every group of agents J ⊆ AGT, let PJ = ⋃i∈J Pi be the set of atomic propositions controlled by the group J. Moreover, for every group J ⊆ AGT and for every set of atomic propositions X ⊆ P, let XJ = X ∩ PJ be the set of atomic propositions in X controlled by the group J. Sets XJ are called J-valuations.

Given a CL-PC model M = (P1, . . . ,Pn,X), the truth condition for the CL-PC modal operators is:

where M ⊕ X′J is the CL-PC model (P1, . . . ,Pn,X′′ ) such that: X′′AGT\J = XAGT\J and X′′ J =X′J . That is, ♦Jϕ is true at a given model M if and only if, the coalition J can change the truth values of the atoms that it controls in such a way that ϕ will be true afterwards (i.e., given the actual truthvalue combination of the atoms which are not controlled by J, there exists a truth-value combination of the atoms controlled by J which ensures ϕ).

4.2 Embedding CL-PC into STIT and CP

The aim of this section is to provide an embedding of CL-PC into the variant of atemporal group STIT with bounded choices (atemporal 'bounded' group STIT) that have been presented in Section 3.1. This is achieved by making use of a suitably defined translation tr2 and dedicated formulae enforcing a CL-PC-like structure on STIT models: formulae EXC + and EXC - enforce that control over atomic propositions in P is exclusive, formula COMPL enforces that exercise of control over atomic propositions in P is complete; formula GRID ∗ enforces that all the possible truth-value combinations of the atomic propositions in P are possible.

Theorem 3. Let m = |P|. Then, a CL-PC formula ϕ is CL-PC-satisfiable if and only if (EXC + ∧ EXC - ∧ COMPL ∧ GRID ∗ ) ∧ tr2(ϕ) is satisfiable in a STIT model where each agent has at most 2m actions.

As CP embeds atemporal 'bounded' group STIT (Theorem 1 in Section 3.1), from Theorem 3 it follows that CP also embeds CL-PC.

5 The Ceteris Paribus Structure of Dynamic Logic of Propositional Assignments

5.1 Logic DL-PA

The dynamic logic of propositional assignments (DL-PA) is the concrete variant of propositional dynamic logic (PDL) [Harel et al., 2000] in which atomic programs are assignments of propositional variables to true or to false. The complexities of the model checking and of the satisfiability problem for DL-PA have been recently studied by [Balbiani et al., 2013]. The starless version of DL-PA was previously studied by [van Eijck, 2000] and recently put to use by [Herzig et al., 2011], who have shown that it embeds CL-PC.

The language of DL-PA is built from a finite set of atomic propositions P and is defined by the following BNF:

We will use ±p to denote (+p ∪ -p). A DL-PAmodel is a set X ⊆ P, that is, a propositional valuation. We provide the semantics for the key operators, the rest is standard: J+pK = {(X,X′ ) | X′ =X ∪ {p}}; J-pK = {(X,X′ ) | X′ =X \ {p}}; J〈π〉ϕK = {X | there exists X′ s.th. (X,X′ ) ∈ JπK and X′ ∈ JϕK}.

We write X |=DL-PA ϕ for X ∈ JϕK. We will refer to the fragment of DL-PA without ∗ operator as starless DL-PA.

5.2 Embeddings between Starless DL-PA and CP

A DL-PA model X can be translated directly to the pointed CP model MCP,X. The desired embedding is obtained through a suitable translation tr3

Theorem 4. Let X be a DL-PA model and ϕ belong to the language of starless DL-PA:

An embedding in the opposite direction can also be obtained, through a suitably defined translation tr4:

From Theorem 5 we can finally obtain as corollary a satisfiability-preserving embedding of CP into DL-PA exploiting a formula GRID∗∗ forcing a CP-model to contain all propositional valuations fromP. Then, tr4(ϕ) is DL-PA satisfiable if and only if GRID∗∗ ∧ ϕ is CP satisfiable.