Epistemic Boolean Games Based on a Logic of Visibility and Control

1 Introduction

Modeling knowledge and decision making are central in multi-agent systems. A key issue is to provide models that are natural and easy to build. Boolean games [Harrenstein et al., 2001; Bonzon et al., 2006; Dunne et al., 2008] were designed with that motivation. There, actions are determined by the agents' control of propositional variables. In that sense, boolean games are easy to build. More recently, they were extended with epistemic goals [ ˚Agotnes et al., 2013] where knowledge is determined by the agents' observation of propositional variables. Several approaches to reasoning about knowledge building on such propositional observability exist in the literature, e.g. [Lomuscio et al., 2000; Su et al., 2007; van der Hoek et al., 2012; van Benthem et al., 2015]. There, epistemic accessibility relations are built in a natural way: agent i cannot distinguish w from w0 when all the variables i sees have the same truth value at w and w0 . A drawback of these approaches is that who sees what is common knowledge: for every variable p and agent i, if i sees p then it is common knowledge that i knows whether p is true; if i does not see p then i's ignorance about p is common knowledge.

There exist only few attempts avoiding this. Some of them suppose that observation comes from geometrical constraints: an agent must physically see another agent in the space [Balbiani et al., 2013a; Gasquet et al., 2014]. A more recent attempt is Dynamic Epistemic Logic of Propositional Assignment and Observation DEL-PAO [Herzig et al., 2015]. It is not grounded on geometrical constraints and thereby allows more flexibility in the description of higher-order visibility. Its language contains special higher-order visibility atoms:

the atom Sip expresses that i sees the value of p; SiSjp expresses that i sees whether j sees p; and so on. It also contains dynamic operators that are based on assignments of propositional variables. The resulting programs modify not only the world, but also the agents' knowledge.

We extend DEL-PAO by adding further special atoms: control atoms. The atom Cip is true if agent i controls the value of p; CiCjp is true if i controls whether agent j controls p; etc. We allow nesting: CiSjp means that i controls j's visibility of the truth value of p; SiCjp that i sees whether j controls p; and so on. A given set of visibility and control atoms determines a Kripke structure in a natural way. This allows to interpret epistemic operators Ki' ("i knows that '") and strategic operators 3J' ("agents in J can change values of variables they control while the other agents do not act so that ' is true"). The latter is an operator of "ceteris paribus strategic ability" in the sense of [van der Hoek and Wooldridge, 2005; Herzig, 2015]. We claim that it is easier for a modeler to describe a situation with visibility and control atoms instead of designing a Kripke structure from scratch. We call our logic DEL-PAOC: Dynamic Epistemic Logic of Propositional Assignment, Observation and Control. In DEL-PAOC, epistemic and strategic operators can be reduced to programs, leading to a sound and complete axiomatization by reduction axioms. Our logic allows to capture epistemic boolean games. While control in such games is both exclusive and exhaustive-each atom is controlled by exactly one agent-we do not impose this in our logic, but can nevertheless reason about it.

The paper is organized as follows. Sections 2 and 3 introduce language and semantics. Sections 4 and 5 provide an axiomatization and complexity results. Section 6 applies DELPAOC to epistemic boolean games. Section 7 concludes.

2 Language

Let Prop be a countable non-empty set of propositional variables and let Agt be a finite non-empty set of agents. Atomic formulas of our language are sequences of visibility and control operators followed by propositional variables.

The set of observability operators is

where Si stands for individual visibility of agent i and JS stands for joint visibility of all agents. The set of control operators is

where Ci stands for control of agent i. The set of all sequences of visibility and control operators is noted (OBS [ CTRL)⇤ and the set of all non-empty sequences is noted (OBS [CTRL)+. We use σ ↪ σ 0 ↪ ▷ ▷ ▷ for elements of (OBS [ CTRL)⇤ . Finally, the set of atomic formulas is:

The language of programs and formulas of DEL-PAOC is defined by the following grammar:

where ↵ ranges over ATM, i over Agt and J over 2Agt . Atomic programs are assignments to atoms: +↵ makes ↵ true and -↵ makes ↵ false. Complex programs are constructed with dynamic logic operators: ⇡; ⇡0 is sequential composition, ⇡t⇡0 is nondeterministic choice, and '? is test. [⇡]' reads "after all executions of ⇡, ' holds"; Ki' and CK' read "i knows that ' on the basis of what she observes" and "all agents commonly know that ' on the basis of what they jointly observe"; 3J' reads "agents in J can achieve ' by modifying variables they control if other agents do not act", which is ceteris paribus strategic ability [van der Hoek and Wooldridge, 2005; Herzig, 2015].

The length of formulas ' and programs ⇡, noted ♣'♣ and ♣⇡♣, is the number of symbols used to write them down, where we do not count [, ], and parentheses and consider that JS, CK, agent names and propositional variables have length 1. The set of atomic formulas of ATM occurring in the formula ' is noted ATM('); the set ATM(⇡) is defined similarly.

The other boolean operators >, ?, _, ! and $ are defined as usual. Moreover, bKi' abbreviates ≻Ki≻', 2J' abbreviates ≻3J≻' and h⇡i' abbreviates ≻[⇡]≻'. The program skip abbreviates >? and fail abbreviates ??.

3 Semantics

Our semantics are based on valuations, or worlds, that are noted w, w0 , u, v, etc. They are subsets of the set of atomic formulas ATM. Then the (unique) model W = 2ATM contains every possible valuation. As it is unique we keep it implicit and only mention the current valuation w in the truth conditions. We write w(↵) = w0 (↵) when ↵ has the same value in w and w0 , i.e., when either ↵ 2 w and ↵ 2 w0 , or ↵ ◁2 w and ↵ ◁2 w0 .

3.1 Strategic Relations

The relation RJ is an accessibility relation for the ceteris paribus strategic operator 3J. It is defined as follows:

Intuitively, only atoms controlled by at least one agent in J can be modified by the coalition J between w and w0 .

3.2 Epistemic Relations and Introspection

We now define accessibility relations ;i and ;Agt allowing to interpret the epistemic operators Ki and CK. These relations are determined by visibility information: two valuations w and w0 are related by ;i if every ↵ that i sees at w has the same value, and similarly for ;Agt . More formally:

The relations ;i and;Agt are reflexive, but they are neither transitive nor symmetric. 1 Transitivity and symmetry are however standard requirements for a logic of knowledge. We will see in the sequel how these constraints can be guaranteed by means of appropriate introspection constraints.

A valuation w 2 2ATM is introspective if and only if the following hold, for every ↵ 2 ATM and i 2 Agt :

The set of all introspective valuations is noted INTR.

Together, the last two constraints ensure that when JS↵ 2 w then σ ↵ 2 w for σ 2 OBS +. This motivates the following relation of introspective consequence between atoms:

↵) β iff either ↵ = β↪ or ↵ = JS↵0 and β = σ↵0 for some σ 2 OBS +▷

Introspective valuations can be characterized as valuations that are closed under introspective consequence.

An atom ↵ 2 ATM is valid in INTR if and only if ↵ belongs to every valuation in INTR. It is shown in [Herzig et al., 2015] that ↵ is valid in INTR iff ↵ is of the form either σSiSi↵ with σ 2 OBS ⇤ , or σ JS↵ with σ 2 OBS +. It is further shown there that the relation;Agt and every relation ;i are equivalence relations on INTR.

We do not have any relations between visibility and control. One might e.g. require that control implies visibility. We will comment on that in the conclusion.

3.3 Truth Conditions and Validity

Given an introspective valuation w, our update operations add or remove atoms. This requires some care: we want the resulting valuation to be introspective. For example, removing SiSip should be impossible. Another example is when w does not contain Sip: then w[¶JSp♦ would violate (C4). So when adding an atom to w we also have to add all its positive consequences. Symmetrically, when removing an atom we also have to remove its negative consequences. Let us define the following:

Clearly, when w is introspective then both w [ E↵ +(↵) and w ∩ E↵ -(↵) are so, too (unless ↵ is valid in INTR).

Truth conditions are standard for boolean operators and:

1 For example, ; ;i w for every w ✓ ATM, while w ;i ; fails to hold as soon as there is a p such that p and Sip are in w.

where R⇡ is a binary relation on valuations that is defined as:

wR⇡1;⇡2 w0 iff there exists u such that wR⇡1 u and uR⇡2 w0

wR'?w0 iff w = w0 and w ♣= '

Lemma 1 ([Herzig et al., 2015]). Let w 2 INTR and wR⇡w0 . Then w0 2 INTR.

Truth conditions are defined on any valuation, including non-introspective ones. However, the intended behavior of the relations R⇡ is not guaranteed in the latter case.

When w ♣= ' we say that w is a model of '. The set of (not necessarily introspective) models of ' is noted k'k.

We note that our epistemic operators behave differently from the standard operators; for a discussion see [Herzig et al., 2015; Charrier et al., 2016].

We generalise validity in INTR from atoms to formulas: a formula ' is valid in INTR if INTR ✓ k'k. It is plainly valid if k'k = 2ATM . Satisfiability in INTR and plain satisfiability are defined analogously. For example, Sip $ (Kip _ Ki≻p) is INTR-valid, but not plainly so.

4 Axiomatics

We are going to reduce epistemic and strategic operators to programs. We then show how to reduce dynamic operators.

4.1 Replacement of Equivalents

The rule of replacement of equivalents preserves validity (both, plain and introspective). It allows us to apply the reduction axioms that we are going to introduce in the rest of the section to the subformulas of a given formula.

Proposition 1. Let '0 be obtained from ' by replacing some occurrence of χ in ' by χ0 . Let w be a valuation. If w ♣= χ$χ0 then w ♣= '$'0 .

4.2 Eliminating Epistemic Operators

The epistemic operators can be eliminated with the help of the following programs:

where A = ¶↵1↪ ▷ ▷ ▷ ↪ ↵n♦ is a finite set of atoms that we suppose ordered in some arbitrary way. The former program tests whether ↵ is seen by agent i; if this is the case then nothing is done, otherwise the truth value of ↵ is nondeterministically set to either true or false. Similarly for the set of all agents:

In both cases, the program is skip when the set A is empty.

Proposition 2. Let ' be without epistemic operators. The following equivalences are valid in INTR:

Proof. The program varyIfNotSeen(i↪ATM(')) is the syntactic counterpart of the definition of ;i, restricted to relevant atomic variables ATM('). Lemma 1 ensures that we do not leave the set of introspective valuations.

4.3 Eliminating Strategic Operators

Strategic operators 3J are reduced to programs in a similar way:

where A = ¶↵1↪ ▷ ▷ ▷ ↪ ↵n♦ is a finite set of atoms that we suppose ordered such that k  l implies that ♣↵k♣  ♣↵l♣. 2 Again, the program is skip when A is empty.

Proposition 3. Let ' be without epistemic operators. The following equivalence is valid in INTR:

Proof. The program varyIfCtrl(J↪ATM(')) is the syntactic counterpart-restricted to relevant atomic variables ATM(')-of the relation RJ between valuations that is used in order to interpret 3J'. Lemma 1 ensures that we do not leave the set of introspective valuations.

For example, the formula

is INTR-valid, where varyIfCtrl(¶i♦↪ ¶p↪ q♦) is the program

So epistemic and strategic operators can be removed, starting from the innermost and using propositions 2 and 3. The result is a formula containing only dynamic operators. The next series of axioms will allow to reduce these.

4.4 Reduction Axioms for Programs

Reduction axioms for programs are standard; we only have to deal with the special case of removing an INTR-valid atom.

2 This is necessary: suppose CiCip is true, and both CiCip and Cip are in A. Then when varyIfCtrl(¶i♦↪Cip) is executed, it will modify Cip non-deterministically, thus being problematic when testing it in varyIfCtrl(¶i♦↪ p) afterwards.

Proposition 4. The following equivalences are plainly valid.

4.5 Axiomatization

The axiomatization of DEL-PAOC is given by:

• ÷ the axioms of CPL (Classical Propositional Logic);
• ÷ the reduction axioms for epistemic, strategic, and dynamic operators of propositions 2, 3, and 4;
• ÷ the introspection axioms respectively noted (VisC1)-(VisC5): SiSi↵, JSJS↵, JSSiSi↵, JS↵ ! Si↵ and JS↵ ! JSSi↵;
• ÷ the rule of Modus Ponens and the rules of inference for Ki, CK, and [⇡]:

Theorem 1. The axiomatization of DEL-PAOC is sound and complete w.r.t. the set of introspective valuations.

Proof. The reduction axioms for epistemic, strategic, and dynamic operators allow to eliminate all modal operators. The resulting formula is INTR-equivalent to the original formula. It is INTR-valid if and only if it is a logical consequence in classical propositional logic of the introspection axioms.

5 Complexity

We define the relevant atoms of a formula ' and a program ⇡ by structural induction as follows:

and homomorphic otherwise. We observe that the cardinality of RATM(') can be exponential in the length of ': for example, the cardinality of the set of atoms RATM(Ki1 ▷ ▷ ▷Kin p) is in 2n .

Given a set of atoms A, a valuation w is introspective w.r.t. A if (i) if ↵ is valid in INTR and ↵ 2 A then ↵ 2 w and (ii) if ↵ 2 w and ↵0 2 E↵ +(↵) \ A then ↵0 2 w.

Proposition 5. For every DEL-PAOC formula ', w ♣= ' iff w \RATM(') ♣= '.

The DEL-PAOC model checking problem is then defined for valuations that are introspective w.r.t. the relevant atoms of the formula under concern:

• ÷ input: a DEL-PAOC-formula ' and a finite valuation w that is introspective w.r.t. RATM(');
• ÷ output: yes if w ♣= ', no otherwise.

Theorem 2. The DEL-PAOC model checking problem is PSPACE-complete.

Proof. For the upper bound, we give a reduction in polynomial time from the DEL-PAOC-model checking problem to the model checking problem of Dynamic Logic of Propositional Assignments DL-PA [Herzig et al., 2011; Balbiani et al., 2013b; 2014]. The reduction transforms a instance (w↪ ') of our model checking problem into a instance (w↪ tr(')) of the DL-PA model checking problem. The translation tr is defined as follows: a DEL-PAOC-formula ' is transformed into a DL-PA-formula tr('), that is, a DEL-PAOC-formula that does not contain any occurrence of Ki, CK and 3J operators. We replace in ' any innermost subformula of the form Ki , CK and 3J by, respectively,

We keep replacing until the resulting formula tr(') does not contain any occurrence of Ki, CK and 3J operators. By propositions 2 and 3, tr(') is equivalent to '.

We define the size of hw↪ 'i as the cardinality of w plus the length of '. Note that the size of tr(') is exponential in the size of ' but is polynomial in the size of the input hw↪ 'i; actually the reduction can be implemented in polynomial time. As the model checking problem of DL-PA is in PSPACE [Balbiani et al., 2014], the DEL-PAOC-model checking problem is in PSPACE, too.

For the lower bound, it suffices to observe that the model checking for DEL-PAO can be trivially reduced to the model checking for DEL-PAOC.

6 Epistemic Boolean Games

We first recall boolean games and epistemic boolean games. We then show how to express in DEL-PAOC that a given valuation is a Nash equilibrium and whether a Nash equilibrium exists.

6.1 Background

Boolean games [Harrenstein et al., 2001; Bonzon et al., 2006; Dunne et al., 2008] are games in which each player wants to achieve a certain goal that is represented by a propositional formula. They correspond to the specific subclass of normalform games in which agents have binary preferences (i.e., payoffs are either 0 or 1) and are widely accepted as a useful and natural abstraction for reasoning about social interaction in multi-agent systems.

A boolean game is a tuple (Agt↪ Prop f ↪ ( i)i2Agt ↪ (γi)i2Agt) where Prop f is a finite subset of Prop, each i ✓ Prop f is the set of variables agent i controls, and γi is a formula of the propositional language such that ATM(γi) ✓ Prop f . The latter expresses i's personal goal, i.e., the state of affairs i wants to achieve. Exclusive and exhaustive control is assumed: the sets i partition the set of variables Prop f . So the two conditions (i) i \ j = ; if i 6= j and (ii) Si2Agt i = Prop f are both satisfied.

A strategy for an agent i, noted si, is an interpretation of variables controlled by i, that is to say, si ✓ i. The set of all possible strategies of agent i is denoted by ⌃i. Given a strategy si for each member of a coalition J, the induced strategy for J is sJ = Si2J si. A strategy sAgt for Agt is called a strategy profile. It can be seen as an interpretation of the set of variables Prop f .

Agent i's utility function maps every strategy profile to i's reward, depending on on the truth value of i's goal in sAgt :

We can express solution concepts such as Nash equilibrium in a boolean game in our logic. Let hsi↪ sAgt∩¶i♦i be the strategy profile composed of the strategy si of i and of the strategy sAgt∩¶i♦ of i's opponents. We say that si is a best response to sAgt∩¶i♦ if and only if, for every strategy s0i 2 ⌃i, Ui(hs0i ↪ sAgt∩¶i♦i)  Ui(hsi↪ sAgt∩¶i♦i) holds. That is, every other strategy of i against the same strategy of opponents would not increase i's reward.

A strategy profile sAgt is a Nash equilibrium, if and only if, for every i 2 Agt, si is a best response to sAgt∩¶i♦. This means every agent cannot get a bigger reward by choosing another strategy if the others do not change theirs.

6.2 Epistemic Boolean Games in DEL-PAOC

An interesting aspect of our logic DEL-PAOC is that it allows us to generalise boolean games to epistemic goals, in the sense of being goals about (own and other agents') knowledge. Agents' goals may now be epistemic formulas: DELPAOC formulas that are built from the propositional variables by the epistemic operators Ki and CK. For example, we can represent the fact that i wants j to know that p is true if and only if agent z knows that p is true by: γi = Kjp $ Kzp. Another example is i's goal that the agents have common knowledge that p, formally: γi = CKp.

We define ATMOBS to be the subset of ATM which only contains propositional variables and atoms about observability of other atoms, that is, atoms beginning with a Si:

An epistemic boolean game is a tuple B = (Agt↪ ATM fOBS ↪ ( i)i2Agt ↪ (γi)i2Agt) where ATM fOBS is a finite subset of ATMOBS , the sets ( i)i2Agt partition ATM fOBS , and every γi is an epistemic formula such that ATM(γi) ✓ ATM fOBS . Strategies of players and coalitions, utilities over strategy profiles, as well as the concept of best response and Nash equilibrium are defined exactly as in the context of standard boolean games.

6.3 Nash Equilibrium in DEL-PAOC

The Nash equilibria of a given epistemic boolean game can be characterised in the language of DEL-PAOC.

Proposition 6. Let B = (Agt↪ATM fOBS ↪ ( i)i2Agt ↪ (γi)i2Agt ) be an epistemic boolean game and let

Then sAgt is a Nash equilibrium for B if and only if

The following proposition provides a characterization in the logic DEL-PAOC of the existence of a Nash equilibrium in a certain epistemic boolean game.

Proposition 7. Let B = (Agt↪ATM fOBS ↪ ( i)i2Agt ↪ (γi)i2Agt ) be an epistemic boolean game. Then B has at least one Nash equilibrium if and only if

The preceding two propositions together with Theorem 2 about complexity of model checking for DEL-PAOC provide a complexity result both for membership problem and for existence problem of Nash equilibria in epistemic boolean games, respectively the problem of checking whether a certain strategy profile is a Nash equilibrium of a given epistemic boolean game and the problem of checking whether a given epistemic boolean game has at least one Nash equilibrium.

Theorem 3. Membership problem and existence problem of Nash equilibria in epistemic boolean games are both in PSPACE.

Proof. From propositions 6 and 7, both problems polynomially reduce to the DEL-PAOC model checking problem.

Let us illustrate epistemic boolean games with an example of coordination game. We note that it cannot be expressed in the framework of [ ˚Agotnes et al., 2013].

Example 1. Suppose we have two agents 1 and 2 each of which knows a bit, respectively noted b1 and b2, that the other agent does not know. Both 1 and 2 have the same goal: K1b2 $ K2b1, that is, 1 wants 2 to know her secret only if 1 knows the secret of 2, and similarly for 2. Each agent can either talk or keep quiet; in other words, each agent has control of the other agent's visibility of her bit. The corresponding epistemic boolean game is Bb = (Agt↪ATM fOBS ↪ ( i)i2Agt ↪ (γi)i2Agt) where Agt = ¶1↪ 2♦, ATM fOBS = ¶b1↪ b2↪ S2b1↪ S1b2♦, 1 = ¶b1↪ S2b1♦, 2 = ¶b2↪ S1b2♦ and γ1 = γ2 = K1b2 $ K2b1.

Indeed, we can show that

Two interesting Nash equilibria are the following. Either they both share their secrets: sAgt = ¶b1↪ b2↪ S2b1↪ S1b2♦; or they both remain silent: sAgt = ¶b1↪ b2♦.

Intuitively, each agent can only modify the other agent's visibility of her secret; if only one of them changes her strategy then it will break the equivalence of the goal.

6.4 Capturing Exclusive and Exhaustive Control in DEL-PAOC

Our logic DEL-PAOC does not impose that control is exclusive. However, the valuations in propositions 6 and 7 where we check whether Nash is true have exclusive and exhaustive control. In this section, we investigate how exclusive and exhaustive control can be built into DEL-PAOC.

First, the set of valuations with exclusive and exhaustive control is:

The set EX is therefore the set of valuations where

is true for every ↵ 2 ATM .

Just as for introspective valuations, we would like to stay in valuations with exclusive control when executing our programs. Direct addition or removal of atoms of the form Ci↵ may lead to worlds outside of EX . We therefore require that control changing programs take the form

reading "i passes the control of ↵ to j".

Lemma 2. Let ⇡ be a program built from nondeterministic choice, sequences, tests and programs of the form i ↵; j. Let w 2 EX and wR⇡w0 . Then w0 2 EX .

Proof. When i ↵; j is executed, ↵ becomes controlled by j only and control of the other atoms remains unchanged.

In epistemic boolean games, exclusive and exhaustive control should not only be preserved by the execution of programs, it should also be common knowledge. We can tune DEL-PAOC to make it common knowledge that control is exclusive and exhaustive. We modify the semantics of DELPAOC so that we restrict to valuations in EX :

We then have to add a test to the programs of Section 4.2 reducing the epistemic operators.

w ♣= CK ΦEX(↵) , for every atom ↵;

Proposition 8. Let ΦEX (') = V↵2RATM(') ΦEX (↵). Then for every w 2 INTR \ EX :

Moreover, under the new truth conditions all the S5 axioms are valid in INTR \ EX. In contrast, plain validity fails for formulas such as the instance of the truth axiom KiΦEX (↵) ! ΦEX (↵).

6.5 Discussion

In [ ˚Agotnes et al., 2013], an alternative concept of epistemic boolean game is introduced and both membership and existence problems for Nash equilibrium in this class of games are studied. However, there is a major difference with our epistemic boolean games: in our class of epistemic boolean games, agents can (i) affect the truth value of propositional variables, and (ii) modify the visibility conditions of propositional variables, including higher-order visibility. For instance, an agent can play a strategy to ensure that another agent can see the truth value of a given propositional variable p or to ensure that another agent can see whether another agent can see the truth value of p, and so on. In ˚Agotnes et al.'s class, agents can only affect the truth value of propositional variables and, indirectly, the knowledge of those agents' who can see the truth value of these variables; but agents cannot modify the visibility conditions of propositional variables. In other words, in ˚Agotnes et al.'s class of epistemic boolean games visibility conditions remain static, whereas in our class they can change. From this perspective, their class of epistemic boolean games can be seen as the subclass of ours where the condition ATM fOBS ✓ Prop holds (i.e., agents can only control propositional variables but cannot control visibility of propositional variables).

˚Agotnes et al. show that for their class of epistemic boolean games, membership and existence of Nash equilibria are PSPACE-complete. In Section 6.3, we have given a complexity result for a more general class of epistemic boolean games.

7 Conclusion

We have studied a dynamic epistemic logic of visibility and control in which one can deduce strategic abilities of coalitions of agents. It accounts for concepts from boolean games such as the existence of a Nash equilibrium that can be extended to epistemic boolean games in a straightforward way. While the complexity of DEL-PAOC satisfiability is open, we have proved that model checking is in PSPACE, which involves reducing the infinite models to finite models involving only the relevant atoms. It follows that the membership problem and existence problem of a Nash equilibria in epistemic boolean games are both in PSPACE. It remains to establish the lower bound.

We claim that our framework can be used in practice easily since visibility information and control information corresponds to what an agents obtain from their sensors.

An interesting variant involving interaction between knowledge and strategies is the requirement 'control implies visibility'. One way of guaranteeing this is to change the condition Si↵? in the program varyIfNotSeen(i↪ ↵) = Si↵? t (≻Si↵?; (+↵t-↵)) of Proposition 2 by (Ci↵^Si↵)?; other constraints can be implemented similarly. A more principled way is to further restrict the set of introspective valuations by imposing constraints such as SiCi↵, for every i and ↵. However, the difficulty here is to redefine INTR such that Lemma 1 still holds. In future work we plan to extend our analysis to iterated boolean games and more generally to repeated interaction.

Acknowledgements. Thanks are due to the IJCAI reviewers for their thorough reading and useful comments.