Verifiable Equilibria in Boolean Games

1 Introduction

Equilibrium selection problems in game theory arise in situations where a game has multiple equilibria, in which case players must make individual choices so as to coordinate on a particular equilibrium [Binmore, 1992, p. 295]. Such problems are particularly important when the failure to coordinate has negative consequences for players. One of the bestknown solutions proposed for the equilibrium selection problem is Schelling's concept of focal points [Schelling, 1980]. Schelling's idea was that some equilibria have distinguishing properties that are independent of their utility structure. A common example is that of two tourists on a day-trip to Paris, who become separated: where should they meet up? The tourists need to independently choose so as to coordinate on a single location; and with respect to utility, any location in the city is as good as any other. But nevertheless, most people suggest the Eiffel tower as a natural meeting place. This is an example of a focal point: an equilibrium that stands out for players in a game, enabling them to coordinate their actions.

We argue that fact that an equilibrium is verifiable can serve to make that equilibrium a focal point. The intuition is as follows. Suppose we have a game with two equilibrium points, A and B, and so players need to coordinate on one of these, and that in terms of utilities, A and B are identical. However, A and B differ with respect to the following property. Equilibrium A carries sufficient information that, if this equilibrium is played, every player will be able to tell that an equilibrium has been played, while B is such that, if it is played, one or more players would be unable to tell for sure that an equilibrium had been played. This, we argue, would be a reason for selecting A rather than B. For, if we chose B, then some players would be unsure whether the actual outcome chosen was indeed an equilibrium. We say that A is a verifiable equilibrium. For a more concrete example, consider the following. Two nations have agreed to eliminate their nuclear weapons, and there are two ways to do this: one of which is verifiable, the other of which is not. Here, the selection of the verifiable course of action is, we believe, more natural for all concerned.

In this paper, we introduce and formalise verifiable equilibria in Boolean games, an increasingly popular game theoretic model, with a natural computational interpretation [Harrenstein et al., 2001; Bonzon et al., 2006; Dunne et al., 2008; Endriss et al., 2011]. In a Boolean game, each player i has under its unique control a set of Boolean variables Φi, from an overall set of Boolean variables Φ. Player i can assign values to variables Φi in any way it chooses: the strategies available to i correspond to the possible Boolean assignments that can be made to variables Φi. The outcome of a Boolean game is a valuation for the variables Φ, made up of the choices of individual players. Each player i has a goal that it desires to be achieved, represented as a propositional formula γi, which may contain variables under the control of other players. Player i is satisfied with an overall outcome if that outcome satisfies γi, and is unsatisfied otherwise. We also assume that each player i is associated with a visibility set, ⇥i ✓ Φ: player i is able to correctly perceive the values of the variables in ⇥i, but cannot observe the values of any other variables [van der Hoek et al., 2011]. We then say that an outcome (v1↪ ▷ ▷ ▷ ↪ vn) for a game is a verifiable equilibrium if it "looks like" a Nash equilibrium to every player-that is, if (v1↪ ▷ ▷ ▷ ↪ vn) could (or would have to) be a Nash equilibrium, given i's view of the outcome (v1↪ ▷ ▷ ▷ ↪ vn) through its visibility set ⇥i. In the remainder of this paper, we formalise several variations of verifiable equilibrium, characterise the complexity of checking for these equilibria, and discuss conditions for their existence. In Section 4, we show how these concepts can be represented using a modal epistemic logic interpreted over our game structures [Fagin et al., 1995].

2 Boolean Games with Incomplete Information

We adapt the basic model of Boolean games [Harrenstein et al., 2001; Bonzon et al., 2006; Dunne et al., 2008; Endriss et al., 2011] to model incomplete information using the idea of visibility sets introduced in [van der Hoek et al., 2011].

Propositional Logic: Let ¶>↪ ?♦ be the set of Boolean truth values, with ">" being truth and "?" being falsity; we use > and ? to denote both the syntactic constants for truth and falsity respectively, as well as their semantic counterparts. Let Φ = ¶p↪ q↪ ▷ ▷ ▷♦ be a finite, fixed, non-empty vocabulary of Boolean variables, and let L denote the set of (well-formed) formulae of propositional logic over Φ, constructed using the conventional Boolean operators ("^", "_", "!", "$", and "≻"), as well as the truth constants ">" and "?". Where ' 2 L, we let vars(') denote the (possibly empty) set of Boolean variables occurring in ' (e.g., vars(p^q) = ¶p↪ q♦). A valuation is a total function v : Φ ! ¶>↪?♦, assigning truth or falsity to every Boolean variable. We write v ♣= ' to mean that the propositional formula ' is true under, or satisfied by, valuation v, where the satisfaction relation "♣=" is defined in the standard way. Let V denote the set of all valuations over Φ. We write ♣= ' to mean that ' is a tautology. We denote the fact that ♣= '$ by ' ⌘ .

Boolean Games: Our games are populated by a set N = ¶1↪ ▷ ▷ ▷ ↪ n♦ of agents-the players of the game. Each agent i is assumed to have a goal, which is represented by an Lformula γi that i desires to have satisfied. Players i each control a (possibly empty) subset Φi of the overall set of Boolean variables. By "control", we mean that i has the unique ability within the game to set the value (> or ?) of each variable p 2 Φi. We will require that each Boolean variable is controlled by exactly one agent, i.e., Φ = (Φ1 [ · · · [ Φn) and Φi \ Φj = ; for all i 6= j. A Boolean game is then defined as a tuple

When playing a Boolean game, the primary aim of an agent i will be to choose an assignment of values for the variables Φi under its control so as to satisfy its goal γi. The difficulty is that the truth-value of γi may depend on variables controlled by other agents j 6= i, who will also be trying to choose values for their variables in Φj to satisfy their own goals; and their goals in turn may depend on the variables Φi.

The set of choices available to an agent i is given by the set Vi of valuations vi : Φi ! ¶?↪>♦ for the variables Φi under his control. Thus, i plays the game by choosing some vi 2 Vi. An outcome is a collection of choices, one for each player. Formally, a strategy profile or outcome for a game is a tuple ~v = (v1↪ ▷ ▷ ▷ ↪ vn) in V1 ⇥ · · · ⇥ Vn. Each outcome uniquely defines an overall valuation for the variables Φ and, given the sets Φ1↪ ▷ ▷ ▷ ↪ Φn, each valuation uniquely defines an outcome. We will, therefore, treat outcomes for games as valuations. We will also often abuse notation and go back and forth between valuations and outcomes, for example writing (v1↪ ▷ ▷ ▷ ↪ vn) ♣= ' to mean that the valuation defined by the outcome ~v = (v1↪ ▷ ▷ ▷ ↪ vn) satisfies formula ' 2 L. The preferences of a player i are captured by a utility function ui : V1 ⇥ · · · ⇥ Vn ! ¶0↪ 1♦ such that for all outcomes ~v,

Thus, the concepts of game theory are readily available to Boolean games as well. This holds in particular for the well-known notion of (pure strategy) Nash equilibrium. We say an outcome (v1↪ ▷ ▷ ▷ ↪ vi↪ ▷ ▷ ▷ ↪ vn) is a Nash equilibrium if there is no player i 2 N and choice wi 2 Vi for i such that ui(v1↪ ▷ ▷ ▷ ↪ wi↪ ▷ ▷ ▷ ↪ vn) > ui(v1↪ ▷ ▷ ▷ ↪ vi↪ ▷ ▷ ▷ ↪ vn). Thus, an outcome is a Nash equilibrium if no player can unilaterally deviate to obtain a better outcome for herself, under the assumption that every other player stays with its choice. We denote the Nash equilibrium outcomes of a game G by N(G); of course, it could be that N(G) = ; for a given game G.

Boolean Games of Incomplete Information: A Boolean game of incomplete information (hereafter simply a "Boolean game" or just "game") is a Boolean game augmented with visibility sets ⇥i ✓ Φ for each agent i. Each agent's visibility set ⇥i indicates that player i is able to correctly observe the values of the variables in ⇥i and no other variables. It is natural to require that each player is able to observe the values of the variables under its control, i.e., Φi ✓ ⇥i for all i 2 N. Note, however, that the results we present below go through without this assumption. Formally, a Boolean game of incomplete information is a tuple

We will denote games by G↪G0 ↪G1↪ ▷ ▷ ▷ etc. If G is such that for every player i 2 N we have ⇥i = Φ then we say that G is a game of complete information. Thus, in a game of complete information, every player can see every variable. We say that an outcome is a Nash equilibrium in a Boolean game of incomplete information if it is a Nash equilibrium in the underlying Boolean game. Thus, the notion of Nash equilibrium is not dependent on the visibility sets ⇥i for players i. The following example illustrates the definitions above.

Example 1 (Two Professors) Two professors and a student have a joint paper accepted at a conference. The question is who of them is going to attend: the first professor (p1), the second (p2), and/or the student (q). Relationships between the professors are a little complicated. Their goals are as follows. Professor 1 wants himself to attend and professor 2 to stay at home; he does not care about the presence of the student. Professor 2's goal is that neither professor goes on his own. The first professor can tell the student what to do. Each professor (only) observes whether himself attends and whether the student attends. We model this situation as a game

with Φ = ¶p1↪ p2↪ q♦; γ1 = p1 ^ ≻p2 and γ2 = ≻(p1 ^ ≻q ^ ≻p2)^≻(≻p1^≻q^p2); Φ1 = ⇥1 = ¶p1↪ q♦ and Φ2 = ¶p2♦ and ⇥2 = ¶p2↪ q♦. The game GG is illustrated in Figure 1.

3 Verifiable Equilibria

We now introduce the idea of verifiable equilibria. The motivation is as follows. A player i is part of a game G. The player can completely see the game-that is, it knows what the variables are, who controls what, and what the goals and visibility sets of each player are. However, when an outcome ~v is chosen, player i can only see the value of the variables in ⇥i. As a consequence, each player has some uncertainty about exactly what actions the other players have performed. We argue that, if the uncertainty is sufficiently large, then players that have actually played a Nash equilibrium collection of choices may in fact have no confidence that this is the case, because they cannot verify the actions of the others. As argued in the introduction, verifiable equilibria can be important in their own right, (such as in the example of nuclear disarmament given in the introduction), and they serve as natural focal points in general. So, we argue, for a Nash equilibrium to be both achievable and verifiable, not only must it satisfy the standard rationality requirements (that no player has any incentive to deviate) but the equilibrium choices of the players must convey sufficient information that each player has confidence that afterwards she can tell that the choices being made constitute a Nash equilibria. We formulate this idea as verifiable feasibility. We will shortly identify and investigate three types of verifiable feasibility; for this we will need some additional notation.

Where ∆ ✓ Φ is a (sub)set of variables in a game G, we define an equivalence relation ⇠∆ over valuations, as follows:

Thus v ⇠∆ w means that the valuations v and w agree on the values of all the variables in ∆. Clearly, this definition induces for every player i 2 N an "indistinguishability" relation ⇠⇥i over valuations. Where there is no risk of confusion, we will write ⇠i as a shorthand for ⇠⇥i . Alert readers will guess that the relations ⇠i will later serve as epistemic accessibility relations [Fagin et al., 1995].

Example 2 (Epistemic indistinguishability in GG) The indistinguishability relations in the game GG are illustrated in Figure 1. Both agents know that in ~v2 both their goals are satisfied. Moreover, they can bring this about, and they know this. Still, they do not know that an equilibrium is played, e.g., since professor 2 considers it possible that the outcome in fact is ~v4, which is not an equilibrium. On the other hand, in ~v1 the outcome is known to be an equilibrium, although it does not satisfy professor 1's goal. Thus, although ~v1 is an equilibrium that can be verified by all players, it is not one that satisfies everybody's goals, whereas~v2 is an equilibrium that makes everybody happy, although it cannot be verified.

Weak Verifiable Equilibrium: We start with the simplest model of verifiable equilibrium. Suppose we are given a game G and an outcome ~v 2 V1 ⇥ · · · ⇥ Vn. We say that ~v is a weak verifiable equilibrium if every player considers it possible that ~v is a Nash equilibrium; that is, if for every player, there is some outcome ~w that is indistinguishable to i from~v such that ~w is a Nash equilibrium. It is important to note that weak verifiable equilibrium does not satisfy our criteria for a verifiable equilibrium, as an outcome ~v being a weak verifiable equilibrium does not mean that ~v is itself a Nash equilibrium. Rather, ~v could be, as far as every player i is concerned. Formally, given game G and an outcome ~v 2 V1 ⇥ · · · ⇥ Vn, we say that ~v is a weak verifiable equilibrium if

Let W(G) denote the weak verifiable equilibria of a game G.

Example 3 (Weak equilibria in GG) In order to compute W(G), given that N(G) = ¶~v1↪~v2↪~v3↪~v5♦ ✓ W(G), we only need to check membership of~v4↪~v6↪~v7, and~v8. In~v8, the outcomes that professor 2 considers possible are ~v8 and ~v6 (in both, p2 and q, the variables that 2 can see, are false). Neither of those outcomes is in N(G), and hence ~v8 62 W(G). Symmetrically, given~v6, professor 2 only considers~v8 and~v6 possible: neither are in N(G), so~v6 62W(G). That ~v7 62W(G) follows similarly. Finally, in~v4, professor 1 considers~v3 possible and professor 2 considers~v2 possible. Since both~v3 and ~v2 are in N(G), we have ~v4 2 W(G).

Let us now establish some basic properties of weak verifiable equilibria.

Proposition 1 1. For all games G, we have N(G) ✓ W(G); for some games, the inclusion is strict.

1. For complete information games G, weak verifiable equilibria and Nash equilibria coincide: W(G) = N (G).
2. For all games G, we have W(G) = ; iff N(G) = ;.
3. If ⇥i = ; for all players i, andN(G) 6= ;, thenW(G) = V.

We now analyse the problem of checking whether an outcome is a weak verifiable equilibrium and find it to be ⌃p2 - complete. The same applies to checking whether the set of weak verifiable equilibria is non-empty.

Theorem 1 Given a game G and an outcome ~v for G, the problem of checking whether ~v 2 W(G) is ⌃p2 -complete;

the problem of determining whether W(G) 6= ; for a given game G is also ⌃p2 -complete.

Proof: For the first part, membership is by guessand-check. For hardness, we reduce the problem of checking whether a Boolean game of complete information has a Nash equilibrium, which is known to be ⌃p2 - hard. Let G be a Boolean game of complete information with n players be given by (N↪Φ↪Φ1↪ ▷ ▷ ▷ ↪Φn↪ γ1↪ ▷ ▷ ▷ ↪ γn), where N = ¶1↪ ▷ ▷ ▷ ↪ n♦. We construct a Boolean game of incomplete information G0 with n + 1 players given by (N[¶n+1♦↪ Φ0 ↪ Φ01 ↪ ▷ ▷ ▷ ↪ Φ0n+1 ↪ γ 01 ↪ ▷ ▷ ▷ ↪ γ 0n+1 ↪ ⇥1↪ ▷ ▷ ▷ ↪ ⇥n+1) where Φ0 = Φ [ ¶a⇤ ♦, a⇤ is a variable not contained in Φ, Φ0i = Φi for all 1  i  n, Φ0n+1 = ¶a⇤ ♦, ⇥i = Φ0i for all 1  i  n + 1, and

Observe that for all ~v = (v1↪ ▷ ▷ ▷ ↪ vn+1) with ~v(a⇤ ) = ?,

To see this, let ~v(a⇤ ) = ? and assume that ~v = (v1↪ ▷ ▷ ▷ ↪ vn+1) 2 N(G0 ). Observe that ~v 6♣= a⇤ and assume (v1↪ ▷ ▷ ▷ ↪ vn) ◁2 N(G). Then, (v1↪ ▷ ▷ ▷ ↪ vn) 6♣= γi and (v1↪ ▷ ▷ ▷ ↪ wi↪ ▷ ▷ ▷ ↪ vn) ♣= γi for some i 2 N and some wi. Then, also ~v 6♣= γi _ a⇤ . Let ~w = (v1↪ ▷ ▷ ▷ ↪ wi↪ ▷ ▷ ▷ ↪ vn↪ vn+1). Then, ~w ♣= γi _ a⇤ . It follows that ~v ◁2 N(G0 ). For the opposite direction, assume ~v = (v1↪ ▷ ▷ ▷ ↪ vn+1) ◁2 N(G0 ). Then, ~v 6♣= γi _ a⇤ and (v1↪ ▷ ▷ ▷ ↪ wi↪ ▷ ▷ ▷ ↪ vn+1) ♣= γi _ a⇤ for some i 2 N [ ¶n + 1♦ and some wi. Since γi = >, we know that i 6= n + 1. Also observe that (v1↪ ▷ ▷ ▷ ↪ wi↪ ▷ ▷ ▷ ↪ vn+1) 6♣= a⇤ and, hence, (v1↪ ▷ ▷ ▷ ↪ wi↪ ▷ ▷ ▷ ↪ vn+1) ♣= γi. Since, vars(γi) ✓ Φ, furthermore, (v1↪ ▷ ▷ ▷ ↪ wi↪ ▷ ▷ ▷ ↪ vn) ♣= γi. It follows that (v1↪ ▷ ▷ ▷ ↪ vn) ◁2 N(G).

To conclude the proof, let ~v0 denote the valuation that sets all variables in Φ0 to ?. We show that,

First, assume that ~v0 2 W(G0 ) and consider player n + 1. Then, there is some ~v = (v1↪ ▷ ▷ ▷ ↪ vn+1) such that both ~v0 ⇠n+1 ~v and ~v 2 N(G0 ). Hence, ~v(a⇤ ) = ? and with (⇤) also (v1↪ ▷ ▷ ▷ ↪ vn) 2 N(G).

For the opposite direction, assume that ~v⇤ = (v⇤1 ↪ ▷ ▷ ▷ ↪ v⇤ n) 2 N(G) and let v⇤n+1 (a⇤ ) = ?. Thus, ~v0 ⇠n+1 (v⇤1 ↪ ▷ ▷ ▷ ↪ v⇤n ↪ v⇤n+1 ). In virtue of (⇤), moreover, (v⇤1 ↪ ▷ ▷ ▷ ↪ v⇤n ↪ v⇤n+1 ) 2 N(G0 ). Finally, let ~v be the valuation that sets all variables in Φ to ? and a⇤ to >. Obviously, ~v satisfies all players' goals. Hence, ~v 2 N(G0 ). Moreover, for all i 2 N, we have ~v0 ⇠i ~v. Thus, for all i 2 N [ ¶i + 1♦, there is some ~w 2 N(G0 ) with~v0 ⇠i ~w and we may conclude that ~v0 2 W(G0 ). 1 2

Note that the problem of verifying whether an outcome of complete information Boolean game is a Nash equilibrium is co-NP-complete, and thus, under standard complexity theoretic assumptions, verifying weak verifiable equilibria is harder than the problem of verifying Nash equilibria in Boolean games of complete information.

1 We are indebted to an anonymous IJCAI reviewer for some simplifications of this proof.

Strong Verifiable Equilibrium: Weak verifiable equilibria do not form a robust basis for action, as the fact that ~v 2 W(G) does not guarantee that ~v 2 N(G). We therefore introduce a stronger notion of verifiable equilibrium. We say ~v is a strong verifiable equilibrium if for every player i and for every outcome ~w that i cannot distinguish from~v, we have that ~w is a Nash equilibrium. Formally, we say that an outcome ~v of a game G is a strong verifiable equilibrium if

We let S(G) denote the strong verifiable equilibria of a game G. It may be readily appreciated that, for every game G, S(G) ✓ N(G), and for some G this inclusion is strict-e.g., for the game GG.

Example 4 (Strong equilibria in GG) We know that S(G) ✓ N(G) = ¶~v1↪~v2↪~v3↪~v5♦. In ~v1, professor 1 considers any outcome possible in which p1 and q are true (~v1 and ~v2), and we know that these outcomes are in N(G). Similarly, in ~v1 professor 2 considers ~v1 and ~v3 possible. These outcomes are also in N(G), hence ~v1 2 S(G). We have ~v2 ⇠2 ~v4 62 N(G), hence ~v2 62 S(G). Similarly, ~v3 ⇠1 ~v4 62 N(G) implies that ~v3 62 S(G). Finally, ~v5 ⇠1 ~v6 62 N(G), hence ~v5 62 S(G). Thus, S(G) = ¶~v1♦.

As with weak verifiable equilibria, strong verifiable equilibria and Nash equilibria coincide under complete information.

Observation 1 If G is a game of complete information, then S(G) = W(G) = N (G).

Theorem 2 Given a game G and an outcome ~v for G, the problem of checking whether ~v 2 S(G) is co-NP complete.

Proof: Membership is by showing the complementary problem is in NP, which can be achieved by guess-and-check. Given a certificate consisting of two outcomes ~v and ~w and two players i and j, it can be checked in polynomial time whether i wants to deviate from~v to ~w, that is, that ~v is not a Nash equilibrium. Moreover it is achievable in polynomial time to check whether player j can distinguish~v and ~w.

Hardness is shown by a reduction of the problem of checking whether a valuation ~v is a Nash equilibrium in a regular Boolean game or not, which is known to be co-NP hard. For a Boolean game G = (N↪Φ↪Φ1↪ ▷ ▷ ▷ ↪Φn↪ γ1↪ ▷ ▷ ▷ ↪ γn) define Boolean game of incomplete information G0 = (N↪Φ↪Φ1↪ ▷ ▷ ▷ ↪Φn↪ γ1↪ ▷ ▷ ▷ ↪ γn↪⇥1↪ ▷ ▷ ▷ ↪⇥n), such that ⇥i = Φ for all players i, i.e., G0 is the Boolean game of complete information corresponding to G. The result follows then immediately from Observation 1. 2

Ideal Verifiable Equilibrium: Finally, we define ideal verifiable equilibria, which are outcomes that are commonly known to be equilibria, when they are played. One can argue that if there is a unique ideal verifiable equilibrium, this will be played: not only do I know that the outcome is an equilibrium, but I do know that you know it, and I know that you know that I know it, etc. Formally, let ⇠C= (Si2N ⇠i)+ (where + denotes transitive closure), and we say that an outcome ~v of a game G is an ideal verifiable equilibrium if

Where G is a game, let I(G) denote the set of ideal verifiable equilibria of G. Clearly, I(G) ✓ S(G) for all G, and this inclusion is strict for some G (e.g., in the following example).

Example 5 (ideal verifiable equilibria in GG) Since

I(G) ✓ S(G) = ¶~v1♦, we only need to check whether outcome ~v1 2 I(G). But since ~v1 ⇠1 ~v2 ⇠2 ~v4 62 N(G), we conclude that ~v1 62 I(G).

Characterising Ideal Verifiable Equilibrium: Ideal verifiable equilibrium is a very strong concept: we will now show that many games do not have one. For this, we first give a characterization of the common knowledge relation ⇠C. Clearly, Ti2n ⇥i is the set of variables visible by all agents. It now turns out that ⇠C is the universal relation on the set of valuations over variables not visible by all agents.

Theorem 3 For all outcomes ~w and ~v of a Boolean game:~w ⇠C ~v iff 8p 2 Ti2N ⇥i : ~v(p) = ~w(p)▷

In other words, two valuations are distinguishable by the common knowledge relation if and only if they disagree on at least one variable that is visible to all agents. This immediately gives us the following characterization of ideal verifiable equilibrium.

Corollary 1 Let G be a game. ~v 2 I(G) iff ~w 2 N(G) for all ~w agreeing with ~v on the variables in Ti2N ⇥i.

As a technical aside, we note that reachability properties (such as common knowledge) are often computationally hard to compute on succinctly represented graphs. Boolean games can be understood as providing a succinct representation for the relation ⇠C, and this might lead one to conclude that computational problems involving these relations would be computationally hard. However, by virtue of Corollary 1, we find that, (perhaps somewhat surprisingly), the ideal equilibrium case is in fact not computationally harder to check than weaker verifiable equilibria.

Theorem 4 Given a game G and an outcome ~v for G, the problem of checking whether ~v 2 I(G) is co-NP-complete.

Considering the set of variables visible to all agents, there are two borderline cases. First, if all variables are visible to all agents, then ideal verifiable equilibrium coincides with standard Nash equilibrium. Second, if no variable is visible to all agents, i.e., if every variable is invisible to at least on agent, ⇠C is the universal relation:

Corollary 2 If Ti2N ⇥i = ;, i.e., if every variable is invisible to at least one agent, then~v ⇠C ~w for all ~w and~v.

In this case an outcome is an ideal verifiable equilibrium if and only if every outcome is an ideal verifiable equilibrium, which in turn holds if and only if every outcome in the game is a Nash equilibrium.

Corollary 3 For any game G, if every variable is invisible to at least one agent then I(G) = ; if N(G) 6= V1 ⇥ · · · ⇥ Vn, and I(G) = N(G) otherwise.

Thus, in the case that every variable is invisible to at least one agent, the games that have ideal verifiable equilibria are exactly those where every outcome is a Nash equilibrium. However, it is, we believe, plausible to assume that there are some commonly visible variables in a game. Indeed, one would intuitively expect that such variables provide the basis around which players will coordinate their actions.

In summary, we have seen that common knowledge of Nash equilibrium is a strong requirement, often difficult to obtain. That common knowledge is difficult to achieve is not surprising, as the situation is similar in related settings; for example in distributed systems where common knowledge is constant in every run [Meyer and van der Hoek, 1995, Corollary 2.2.6], and in public announcement games [ ˚Agotnes and van Ditmarsch, 2011] where common knowledge of nontrivial Nash equilibria is impossible. Our framework demonstrates this once again.

4 Logical Characterisation

We now show how the Epistemic Coalition Logic of Propositional Control ("ECL" for short) can be used to characterise and reason about the concepts we have introduced above. Introduced in [van der Hoek et al., 2011], ECL combines the well-known modal epistemic language S5 C n [Fagin et al., 1995] with operators allowing us to represent the choices available to agents [van der Hoek and Wooldridge, 2005]. The language of ECL extends classical propositional logic with modal operators Ki and C for referring to the knowledge possessed by agents. A formula Ki', where i 2 N is an agent, is to be read "agent i knows that '", while a formula C' is to be read "it is common knowledge that '". In addition, the language contains operators 3i', where i 2 N, with the intended interpretation that "assuming nothing else changes, then i has a choice such that ' holds". More precisely, 3i' means that i can assign values to the variables under its control in such a way as to make ' true.

Formally, the syntax of formula ' of ECL is defined with respect to a set N = ¶1↪ ▷ ▷ ▷ ↪ n♦ of agents and a set Φ = ¶p↪ q↪ ▷ ▷ ▷♦ of Boolean variables by the following grammar:

We now give an interpretation of formulae of ECL with respect to pairs of the form (G↪~v), called pointed games, where G is a game (with player set N and variable set Φ) and ~v is an outcome for G. We write (G↪~v) ♣=ECL ' to mean that the formula ' is true with respect to (G↪~v), defined as follows:

Other propositional connectives (^↪!↪ ▷ ▷ ▷) are defined in terms of ≻ and _ in the standard way. We also define E' = Vi2N Ki' ("everyone knows that '"). The model checking problem for ECL is as follows: we are given a pointed game (G↪~v) and a formula ', and asked whether (G↪~v) ♣=ECL '.

We now show how weak, strong and ideal verifiable equilibria can be quite naturally captured as formulae of our epistemic language. First, where G is a Boolean game, we define an ECL formula ⌫(G) (or just ⌫) as follows:

The key point about ⌫ is that it characterises Nash equilibria: Proposition 2 For all pointed games (G↪~v), we have:

(G↪~v) ♣=ECL ⌫ iff ~v 2 N(G).

Next, for each game G we define the following formulae:

(We omit G when clear from context). With these definitions in place, we can state our logical characterisation results.

Proposition 3 For all Boolean games G and outcomes~v: ~v 2 W(G) iff (G↪~v) ♣=ECL υ; ~v 2 S(G) iff (G↪~v) ♣=ECL σ; ~v 2 I(G) iff (G↪~v) ♣=ECL .

Thus, the problem of checking verifiable equilibria can be reduced to ECL model checking problems.

Example 6 (Logical properties of GG) In the game GG, we have (GG↪~v4) ♣=ECL ≻γ1 ^ ≻⌫ ^ ≻K1≻⌫ ^ ≻K1⌫ ^ Cq: professor 1's goal γ1 is not satisfied in ~v4; ~v4 is not a Nash equilibrium; professor 1 considers this possible, but he does not know it; and it is common knowledge that q holds. Also, (GG↪~v1) ♣=ECL γ2 ^ ≻γ1 ^ ⌫ ^ E⌫ ^ ≻C⌫: ~v1 satisfies professor 2's goal but not professor 1's; v1 is a Nash equilibrium and everybody knows this, still it is not common knowledge.

Normal Forms: Above we gave a new interpretation of ECL. We now turn to studying the resulting logic in more detail. Although the object language seems rather rich, we will now argue that in fact every formula ' of ECL is equivalent (on games) to a formula in propositional logic. More precisely, for every ' of ECL there is a formula ⇡ in propositional logic such that (G↪~v) ♣=ECL ' iff ~v ♣= ⇡.

We have to leave out the formal proof of this due to lack of space, and instead sketch the idea here based on examples. Let '(p1↪ ▷ ▷ ▷ ↪ pk) be a formula where p1↪ ▷ ▷ ▷ ↪ pk are all the variables fromΦi that occur in ' and let '(b1↪ ▷ ▷ ▷ ↪ bk) denote ' with bi 2 ¶?↪ >♦ uniformly substituted for pi. Then

For examples, let us use atoms pi↪ qi↪ ▷ ▷ ▷ to denote they are in Φi. Then, 31(p1 ^ (p2 _ q2)) ⌘ECL (? ^ (p2 _ q2)) _ (>^ (p2 _ q2)) ⌘ECL p2 _ q2. Indeed, if Φ1 = ¶p1♦, then for agent 1 to enforce p1 ^ (p2 _ q2), he needs to rely on the truth of those variables not in Φ1, i.e., on (p2_q2). Similarly, 3132(p1 ^≻p2 ^p3)) ⌘ECL p3 ⌘ECL 31(p1 ^3(p2 ^p3)).

Let '(q1↪ ▷ ▷ ▷ ↪ qm) be a formula where q1↪ ▷ ▷ ▷ ↪ qm are all the variables in Φ ∩ ⇥i occurring in '. Then,

For example, suppose ⇥1 = ¶p↪ q♦ and ⇥2 = ¶q↪ r♦, while Φ = ¶p↪ q↪ r↪ s♦. Then K1(p^q) ⌘ECL (p^>)^(p^?) ⌘ ?: Indeed, 1 cannot know that q since q 62 ⇥1. For another example, K1(K2q ^ (K2r _ K2≻r)) ⌘ECL q. If ⇥1 = ¶p↪ s♦ and ⇥2 = ¶q↪ r♦, then K231(p ^ (q _ r)) ⌘ECL K2r ⌘ECL r while K131(p ^ (q _ r)) ⌘ECL K1r ⌘ECL ?. For instance, note that we are not saying that K2r $ r is a validity over all games even if it is true in games where r 2 ⇥2.

Since we have only a finite number (say k) of atoms, and the alternatives for the agents are valuations, we can finally replace every C' by E' ^ EE' ^ ▷▷▷ ^ EE ▷ ▷ ▷ E', where the number of E operators in the last conjunct is 2k .

This all implies that we do not need our rich object language to reason about even epistemic properties of Nash equilibria if we are only interested in expressivity. However, it is clear that the formulae of our object language are much more succinct than the equivalents we obtain in propositional logic.

5 Conclusions

In this paper, we proposed that verifiability can provide a means to distinguish between equilibria that are otherwise similar. We formalised verifiable equilibria by extending the standard model of Boolean games with sets of visible variables. As a consequence, players don't necessarily know which outcome they have ended up in. We formalised and studied three variants of verifiable equilibria. We characterised the complexity of computing them, gave conditions for their existence, and demonstrated how they can be characterised using modal logic. We emphasise that while we argue that verifiable equilibria are natural focal points, that does not mean that verifiable equilibria always are more reasonable than non-verifiable equilibria - there might be other reasons for selecting non-verifiable equilibria. For example, a game might have a non-verifiable equilibrium that consists of dominant strategies in addition to a verifiable equilibrium. The point is that verifiability can provide a solution to the problem of choosing between equilibria that otherwise are similar.

We looked at both strong verifiable equilibria, where all players know a posteriori that they are in an equilibrium, as well as ideal verifiable equilibria, where (in addition) it is common knowledge that an equilibrium has been played. In particular, we saw that the latter occur only in very special cases. It is important to note that the difference here is in the definition of verifiability: in the former case each agent knows that the outcome is an equilibrium but not necessarily that the other agents know that, unlike in the latter case. But in both cases it is common knowledge before the outcome is chosen, which outcomes are (strong or ideal) verifiable equilibria. The assumptions underpinning game theory with respect to what players in a game know about the game and each other, and the impact of relaxing or modifying these assumptions with respect to the outcomes of games that are predicted by game theoretic solution concepts, are studied in the field of epistemic game theory [Pacuit and Roy, 2012]. However, in this paper we are concerned with incomplete information about the outcome, i.e., about the actions chosen by all players in the situation after the players have acted.

For future research, it would be of interest to find more computationally tractable classes of games. We believe that the general framework in Section 4 can be used towards that end. Furthermore, other possible solution concepts can be of interest, taking the players' knowledge of whether or not they will be better off into account when defining best responses.