Iterated Boolean Games

1 Introduction

Playing a game more than once against the same opponent can have a dramatic effect on which outcomes of the game can be sustained as equilibria [Osborne and Rubinstein, 1994, pp.133-161]. To take a classic example in the literature, in the one-shot Prisoner's Dilemma there is a unique pure Nash equilibrium in which both players defect, leading to payoffs that are worse for both players than the payoffs they would have obtained had they cooperated. However, cooperation cannot be ensured in the one-shot Prisoner's Dilemma. If, instead, the same players repeatedly meet each other then cooperation can be sustained-leading to equilibria (outcomes) which can be better than those of the one-shot version of the game. Cooperation is rationally sustainable because the players will meet in the future, and will thereby have the opportunity to punish each other for non-cooperation.

We study iterated versions of Boolean games. The basic idea of a Boolean game [Harrenstein et al., 2001] is that each player i is associated with a goal, represented as a logical formula γi, and player i's main purpose is to ensure that γi is satisfied. The strategies and choices for each player i are defined with respect to a set of Boolean variables Φi, drawn from an overall set of variables Φ. Player i is assumed to have unique control over variables Φi, in that it can assign truth values to these variables in any way it chooses. Strategic concerns arise in Boolean games as the satisfaction of player i's goal γi can depend on the variables controlled by other players.

In the version of Boolean games that we study, it is assumed that players interact over an infinite series of rounds, where at each round each player makes an assignment to the variables under its control. Goals are expressed as formulae of Linear Temporal Logic (LTL), a well-known formalism for expressing properties of distributed and concurrent systems [Emerson, 1990; Manna and Pnueli, 1992; 1995]. Formulae of LTL are essentially predicates over infinite sequences of states. Thus, whether a player's goal is or is not satisfied may depend not just on how players act on one round, but how they act in all future rounds.

Players in Boolean games can be understood as nondeterministic computer programs, and the model thus has great relevance to multi-agent systems research. As players can model programs, building strategies in Boolean games corresponds to synthesising computer systems from their logical specifications, for instance as the modules for control and synchronisation of concurrent processes [Kupferman et al., 2000; Vardi, 2008; Pnueli and Rosner, 1988].

The paper contains three main contributions. Firstly, it formalises iterated Boolean games. Moreover, it provides a finite state machine representation (an operational model) along with a temporal logic theory (a denotational model) for the strategies and players. This dual operational/denotational model for iterated Boolean games allows us to investigate computational properties regarding the games, such as whether a collection of strategies forms a Nash equilibrium.

Secondly, we study the complexity of various decision problems. Model checking for iterated Boolean games is in PSPACE and thus no harder than model checking for LTL [Sistla and Clarke, 1985]. Synthesis is 2EXPTIME-complete, matching the complexity of synthesis for 'rational systems' [Fisman et al., 2010]. Moreover, checking whether a strategy profile is a pure Nash equilibrium and whether a game has at least one pure Nash equilibrium are complete problems for PSPACE and 2EXPTIME, respectively.

Thirdly, we give Folk Theorems for iterated Boolean games. These theorems provide semantic characterisations of LTL properties that are satisfied in equilibrium outcomes. Some of these Folk Theorems completely characterise games for which some questions can be answered more efficiently; in particular, synthesis can be done in PSPACE.

Relatedwork Equilibria in Boolean games have been studied before (e.g., [Dunne et al., 2008; Bonzon et al., 2009; Grant et al., 2011]) but, to our knowledge, not in models where the players are assumed to interact for an infinite number of rounds, which is the setting our results pertain to.

However, there are many games in the computer science literature where the plays have infinite length; see, e.g., [Chatterjee and Henzinger, 2012; Gr¨adel and Ummels, 2008] for surveys on the topic. These games are most usually played by two players (together with a hostile environment) who display independent, distributed, and concurrent behaviour. In our setting, we are interested in situations where there are multiple players who do not necessarily have opposing objectives: in fact cooperation is a desirable behaviour in our setting.

Folk Theorems for other games are mostly found in the game theory literature rather than in computer science or multi-agent systems research. Yet there are a few exceptions. In [Fisman et al., 2010] a similar question is asked for a problem-rational synthesis-that is essentially one of the decision problems for iterated Boolean games. Other results on synthesis can be found too, see, e.g., [Chatterjee et al., 2008; Ummels, 2006; Lustig and Vardi, 2009; Kupferman et al., 2000]. In most of this literature the emphasis is on the question of whether a particular LTL formula can be synthesised. With the Folk Theorems, on the other hand, the focus is on semantic representations of complete classes of properties (LTL properties in this case) which can be rationally sustained-and hence possibly synthesised.

2 Preliminaries

Let Φ = {p, q, . . .} be a (finite, fixed, non-empty) set of Boolean variables and L0 the set of formulae of classical propositional logic constructed over Φ. A valuation v is a subset of variables, that is, v ⊆ Φ, where it is understood that v assigns truth to all the variables it contains and falsity to the others. Let V be the set of valuations for Φ. For formulae ϕ ∈ L0 we use v |= ϕ to indicate that v satisfies ϕ.

Linear Temporal Logic (LTL): LTL extends classical propositional logic with modal tense operators X ("next"), F ("eventually"), G ("always"), and U ("until"), which can be used for expressing properties of sequences. We take X and U as our atomic operators, and define the remaining LTL connectives based on these. The syntax of LTL is defined with respect to a set Φ of Boolean variables as follows:

where p ∈ Φ. The remaining classical and LTL connectives are then defined in the standard way; in particular, we have Fϕ = ⊤Uϕ, and Gϕ = ¬F¬ϕ. Given a set of variables Ψ, let L(Ψ) be the set of LTL formulae over Ψ.

A core concept in the semantics for LTL is that of a run. A run ρ: N → V is a function that assigns a valuation ρ[t] to every time point t ∈ N, indicating which Boolean variables are true at time t. 1 We interpret formulae of LTL with respect to pairs (ρ, t), where ρ is a run and t ∈ N is a temporal index into ρ. Formally, the semantics of LTL formulae is as follows:

1 We use square brackets for parameters referring to time points.

If (ρ, 0) |= ϕ, we also write ρ |= ϕ and say that ρ satisfies ϕ. We say that ϕ and ψ are equivalent if for all runs ρ we have ρ |= ϕ if and only if ρ |= ψ. An LTL formula ϕ ∈ L is satisfiable if there is some run satisfying ϕ.

3 The game model

Variables, Control, and Choices: Each player i controls a (possibly empty) subset Φi of the overall set of Boolean variables. That is, player i has the unique ability to choose the value (either true or false) of each variable p ∈ Φi at each round of the game. A choice for agent i ∈ N is a subset vi of the propositional variables under his control, i.e., vi ⊆ Φi. At every round of the game, each player makes such a choice. Let Vi be the set of choices for agent i. A choice vector ⃗v is a collection of choices, one for each player, that is, ⃗v = (v1, . . . , vn). A choice vector uniquely defines an overall valuation for Φ, and vice versa. We will generally abuse notation by treating choice vectors as valuations and valuations as choice vectors. Every choice vi and every choice vector ⃗v is associated with a characterising formula χΦi vi = ∧p∈Φi∩vi p ∧ ∧p∈Φi\v ¬p and χΦ ⃗v = ∧i∈N χΦvi .Thus, ⃗v |= χΦ ⃗w if and only if ⃗v ∩ Φ = ⃗w ∩ Φ. We will omit the superscripts whenever Φ and Φi are clear from the context.

Iterated Boolean Games: An Iterated Boolean Game (hereafter sometimes just called a "game") is a structure:

where N = {1, . . . , n} is a set of players, Φ = {p, q, . . .} is a finite set of Boolean variables 2 , Φi ⊆ Φ is the set of Boolean variables under the unique control of player i, and γi ∈ L is the LTL goal of player i.

There is one requirement on these structures: the sets of Boolean variables Φ1, . . . , Φn must form a partition of Φ, that is, Φi ∩ Φj = ∅ for all i ̸= j ∈ N and Φ = Φ1 ∪ · · · ∪ Φn.

The outcomes of a game are given by the runs ρ ∈ R. Each player i is associated with a strict preference relation ≻i over the runs. Every relation ≻i is binary in the sense that player i strictly prefers runs that satisfy its goal γi over runs that do not and is indifferent otherwise, that is, for all runs ρ and ρ′ ,

Moreover, ρ ≿i ρ′ means that it is not the case that ρ′ ≻i ρ.

2 Arbitrary finite domains can be represented by Boolean domains-viz., as finite numbers are represented by binary ones.

Strategies: In a one-shot Boolean game, a strategy for a player i is simply a single choice vi ∈ Vi. This is, of course, not the case for iterated Boolean games. In iterated Boolean games, a strategy for player i is a function that makes a choice in each round of the game on the basis of the history of the game to date. Formally, we can understand such strategies as functions fi : V ∗ → Vi, where V ∗ denotes the set of finite sequences over V. In order to study computational problems for games, it is desirable to have a finite representation for strategies: here we model strategies as deterministic finite state machines. Such representations are widely used to study repeated games in the game theory literature [Osborne and Rubinstein, 1994, p.140-143] and are of course very natural from a computational point of view. Formally, a machine strategy σi for player i in a game G = (N, Φ, Φ1, . . . , Φn, γ1, . . . , γn) is given by a structure:

where Qi is a finite, non-empty set of states, q0i is the initial state, δi : Qi × V → Qi is a state transition function, and τi : Qi → Vi is a choice function. Let Σi denote the class of strategies for player i. It is implicit above that δi is a total function, and so, for any given state q ∈ Qi we must have δi(q, v) defined for all 2|Φ| valuations v ∈ V, resulting in machine strategies of size exponential in |Φ|.

To obtain a more compact representation, we may allow the transition function δi to be a partial function. Such a partial strategy σi = (Qi, q0i , δi, τi) then represents the (complete) strategy σ′ = (Qi ∪{q d i }, q0i , δ′ , τ ′ i ), where q d i is an additional "default state" to which δ′ in state q and valuation⃗v maps, in case δ(q, v) is undefined. Moreover, τ ′ (q d i ) = ∅. This will relieve us of the need to explicitly define δi(q, v) for every v: we only need to define δi(q, v) for the valuations v of interest.

A strategy profile ⃗σ is an n-tuple of strategies, one for each player i, that is, ⃗σ = (σ1, . . . , σn). For S ⊆ N, define (⃗σ-S , ⃗σ′S ) as the strategy profile ⃗σ′′ such that σ′′ i = σi if i /∈ S and σ′′ i = σ′ i otherwise. If S = {i} we omit the curly braces and write (⃗σ-i , σ′ i ) rather than (⃗σ-{i} , σ′{i} ).

Because strategies are deterministic, each ⃗σ induces a unique run, denoted by ρ(⃗σ). To define ρ(⃗σ), we need some notation. First, a state vector of a strategy profile is a tuple ⃗q = (q1, . . . , qn), where, for all i ∈ N, we have qi ∈ Qi. With each point of time t we associate both a state vector denoted by ⃗q[t] = (q1[t], . . . , qn[t]) and an outcome denoted by ⃗v[t] = (v1[t], . . . , vn[t]). The history h(⃗σ) of ⃗σ is an infinite sequence of interleaved state vectors and outcomes:

where:

and for all t ∈ N such that t > 0 we have:

Note that machine strategies provide an operational model for the behaviour/interactions of the players in a game. The following lemma will prove very useful and is a consequence of standard expressivity results (see, e.g. [Thomas, 1990; Diekert and Gastin, 2008]) for LTL with respect to languages accepted by deterministic ω-automata.

Lemma 1 For every satisfiable LTL formula ϕ there is a strategy profile ⃗σ = (σ1, . . . , σn) such that ρ(⃗σ) |= ϕ.

As LTL can express every finite star-free ω-regular language and a run ρ(⃗σ) for a strategy profile ⃗σ can be seen as an ω-regular word over the valuations V over Φ, it can readily be appreciated that for every strategy profile ⃗σ there is an LTL formula ϕ(⃗σ) such that for all runs ρ,

Then, the LTL formula ϕ(⃗σ) exactly characterises the unique run ρ(⃗σ) induced by the strategy profile ⃗σ (the formula ϕ(⃗σ) holds on ρ(⃗σ) and only on ρ(⃗σ)). The formula ϕ(⃗σ), however, may be exponential in the size of ⃗σ. We thus also have a lemma which ensures that every run ρ(⃗σ) is characterised by an LTL formula that is polynomial in the size of ⃗σ.

For each player i and each state qi ∈ Qi introduce a new ("fresh") Boolean variable which, assuming Φ, Q1, . . . , Qn to be pairwise disjoint, we will also denote by qi. Moreover, we use Q = Q1 ∪ · · · ∪ Qn to refer to the entire set of these new variables. For every player i and every (complete) strategy σi we define an LTL formula th(σi) ∈ L(Φ ∪ Q) as follows:

where,

Let furthermore TH(⃗σ) = ∧i∈N th(σi) for strategy profiles ⃗σ = (σ1, . . . , σn). Observe that th(σi) is polynomial in the size of σi; for partial strategies a similar formula can be defined, still polynomial in size. Intuitively, th(σi) is the LTL theory of strategy σi: the property INIT(σi) encodes the initial state q0i , TRANS(σi) encodes the transition relation δi, INVAR(σi) ensures that the strategy is in exactly one state at any given time, while VAL(σi) encodes the choice function τi. Thus, th(σi) provides a denotational model for σi with respect to the semantics of LTL. In particular, for all ρ: N → 2Φ∪Q satisfying TH(⃗σ) it holds that ρ[t]∩Φ = ρ(⃗σ)[t] for all t ∈ N, i.e., the run ρ restricted to Φ coincides with ρ(⃗σ).

Formulae of the form th(σi)-which characterise the players' behaviour-are satisfiable, as shown next.

Lemma 2 Let ⃗σ = (σ1, . . . , σi) be a strategy profile and let S ⊆ N. Then, ∧i∈S th(σi) is satisfiable.

Based on the same construction, the following lemma holds.

Lemma 3 Let ⃗σ be a strategy profile in the game

Then, for all S ⊆ N and all ϕ ∈ L(Φ), we have that

∧ i∈S th(σi) ∧ ϕ is satisfiable implies ρ(⃗σ′-S , ⃗σS ) |= ϕ for some ⃗σ′ .

Nash Equilibrium: Let us now define the well-known notion of (pure strategy) Nash equilibrium for iterated Boolean games, which will allow us-in the next section-to ask different computational questions about these games. A strategy profile ⃗σ is defined to be a (pure strategy) Nash equilibrium if for all players i ∈ N and for all strategies σ′ i ∈ Σi we have

Let NE(G) denote the set of Nash equilibria of game G.

Due to the binary character of the players' preferences, our definition implies that the strategy profile ⃗σ is a Nash equilibrium if every player whose goal is not satisfied by the run ρ(⃗σ) cannot unilaterally deviate and get its goal achieved.

Observation 4 Strategy profile ⃗σ is a (pure strategy) Nash equilibrium if and only if for every player i ∈ N,

either ρ(⃗σ) |= γi or for all σ′ i ∈ Σi: ρ(⃗σ-i, σ′ i ) ̸|= γi.

4 Complexity

We now consider the computational complexity of problems relating to Nash equilibria in iterated Boolean games. We first establish an upper bound on the complexity of a problem that underpins many of others that we will study later on:

Given: Game G, profile ⃗σ, and LTL formula ϕ. MODEL CHECKING: Is it the case that ρ(⃗σ) |= ϕ?

This problem is not quite the same as the "standard" LTL model checking problem, which is known to be PSPACEcomplete ("truth in an R-structure" [Sistla and Clarke, 1985, p.741]), and so we need to establish the upper bound.

Proposition 5 MODEL CHECKING is in PSPACE.

Proof sketch: We reduce MODEL CHECKING to LTL satisfiability checking, which is known to be in PSPACE [Sistla and Clarke, 1985]. Let ϕ ∈ L(Φ). To check whether ρ(⃗σ) |= ϕ, we simply ask whether TH(⃗σ) ∧ ϕ is satisfiable. Recall that the size of TH(⃗σ) is polynomial in the size of ⃗σ. It suffices to show that, TH(⃗σ) ∧ ϕ is satisfiable if and only if ρ(⃗σ) |= ϕ. The implication from left to right is immediate by Lemma 3 (for S = N). For the opposite direction, by Lemma 2, we have ρ(⃗σ′ ) |= TH(⃗σ) for some ⃗σ′ . Lemma 3 then yields ρ(⃗σ′ ) |= ϕ and the result follows.

With this result in place, we can move on to consider problems specifically related to equilibria in iterated Boolean games. First, consider the following problem:

Given: Game G, strategy profile ⃗σ. MEMBERSHIP: Is it the case that ⃗σ ∈ NE(G)?

Using Observation 4, and the construction th(σi) for strategies σi-the denotational model for machine strategies-that was given before, we have the following result.

Proposition 6 MEMBERSHIP is PSPACE-complete.

Proof sketch: We give an algorithm that is in PSPACE and solves MEMBERSHIP for iterated Boolean games:

1. for i := 1 to n do 2. if ρ(⃗σ) ̸|= γi then 3. if γi ∧ ∧j∈N\{i} th(σj) is satisfiable then 4. return "no" 5. end-if 6. end-if 7. end-for

1. return "yes"

Because of Proposition 5, we know that line (2) can be solved using a PSPACE oracle for MODEL CHECKING; moreover, line (3) uses a PSPACE oracle for satisfiability.

The algorithm checks whether there is some player i such that ρ(⃗σ) ̸|= γi and γi ∧ ∧j∈N\{i} th(σj) is satisfiable. It outputs "no" if this is the case and "yes," otherwise. Soundness follows immediately from Lemma 3 and Observation 4.

For hardness, reduce LTL satisfiability to MEMBERSHIP. Let ϕ be an LTL formula in L(Φ) and let ρ0 be the run such that ρ0 [t] = ∅ for all t ∈ N. Without loss of generality, we may assume that ρ0 ̸|= ϕ. Define G as the oneplayer iterated Boolean game in which player i has ϕ as goal. Let σi = (Qi, q0i , δi, τi) be the partial machine strategy with Qi = {q0i } and δi = τi = ∅. Thus, ρ(σi) = ρ0 and ρ(σi) ̸|= ϕ. Clearly, σi is polynomial in the size of ϕ. It can now readily be appreciated that ϕ is satisfiable if and only if σi /∈ NE(G). As PSPACE is closed under complement, the result follows.

Thus, checking membership is no more complex than LTL model checking. However, other apparently closely related problems turn out to be much harder. Consider the following:

Given: Game G, LTL formula ϕ ∈ L. E-NASH: Does ∃⃗σ ∈ NE(G). ρ(⃗σ) |= ϕ hold? Given: Game G, LTL formula ϕ ∈ L. A-NASH: Does ∀⃗σ ∈ NE(G). ρ(⃗σ) |= ϕ hold? Given: Game G.

NON-EMPTINESS: Is it the case that NE(G) ̸= ∅?

E-NASH is basically the rational synthesis problem for pure Nash equilibrium as first analysed by Fisman et al, whose complexity is 2EXPTIME-complete (Theorem 2 in Fisman et al [Fisman et al., 2010]) 3 . Since 2EXPTIME is a deterministic complexity class, 2EXPTIME-completeness of A-NASH immediately follows as a corollary.

Proposition 7 ([Fisman et al., 2010]) Both A-NASH and ENASH are 2EXPTIME-complete.

We can now show that NON-EMPTINESS is also complete for 2EXPTIME. For membership we ask whether (G,⊤) is accepted as an instance of E-NASH; for hardness we reduce the LTL realizability problem [Pnueli and Rosner, 1989b], which is known to be 2EXPTIME-complete.

Proposition 8 NON-EMPTINESS is 2EXPTIME-complete.

3 Although we consider machine strategies rather than strategies as functions between partial plays, our strategy model is known to be sufficiently powerful for LTL goals [Pnueli and Rosner, 1989a].

5 Folk Theorems

In game theory much of the interest in iterated games derives from the Nash Folk Theorems [Osborne and Rubinstein, 1994, p.143]. These theorems tell us that the range of outcomes that can be sustained as equilibria in iterated games is much wider than one might at first suspect from the component game. Their usual form is that the set of all feasible and individually rational payoff vectors are achievable as Nash equilibria in iterated games; the definitions of feasibility and individual rationality depend on the precise setting considered.

To take a famous example, the Nash Folk Theorems tell us that cooperation can be sustained in the iterated Prisoner's Dilemma. The standard device for proving Folk Theorems is a trigger strategy [Osborne and Rubinstein, 1994, p.143]. A trigger strategy intended to obtain a particular outcome works by punishing any player who deviates from behaviour leading to the intended outcome: no player can benefit from deviation, as this would result in punishment by all other players. The desired outcome is thereby obtained as an equilibrium.

It seems very natural, therefore, to consider Folk Theorems in the context of our iterated Boolean games. Given our interest in using LTL to express properties of equilibria, we can formulate the question of which equilibria can be sustained in an iterated Boolean game in the following way:

Which LTL properties are preserved by the Nash equilibria of a given iterated Boolean game?

This question is closely related to the rational synthesis problem proposed by [Fisman et al., 2010], and here formalised in the E-NASH problem. However, the rational synthesis problem, in effect, pertains to particular LTL properties being realised in some Nash equilibrium, while our concern is rather with characterising the set of LTL formulae that can be satisfied in equilibria of iterated Boolean games.

In this section, we show that the concepts and techniques used to prove the Nash Folk Theorems can be adapted to our setting. In particular, for games in which players have safety goals (of the form Gϕ), we use a punishment strategy construction, similar in spirit to that used to prove the Nash Folk Theorems, to characterise precisely the circumstances under which arbitrary LTL formulae are satisfied in some equilibrium of an iterated Boolean game.

To be able to use such a construction, we need to be able to define for our setting some counterpart of the notion of a feasible and individually rational payoff for each player. In game theory, a payoff is individually rational and feasible if it could be enforced by the set of all other players in the game. In our setting, players have goals, rather than payoffs, and so we need to formulate the concept with respect to whether a player's goal can be falsified by the set of all other players.

Punishable players and goals A player i, with goal γi, is punishable if (at any point of time) i's opponents can jointly find values for the propositional variables under their control that guarantee γi to be false no matter which values i chooses for its variables. Nash Folk Theorems may hold only if all players, at all times, are punishable. This is indeed the case for games with certain kinds of goals, which we define next.

We say a goal γi is non-trivial if both γi and ¬γi are satisfiable (i.e., γi is neither a tautology nor a contradiction in LTL). We say γi is a safety goal when γi = Gϕi for some LTL formula ϕi. When ϕi is a propositional formula we say that γi is a propositional safety goal. Folk theorems for iterated Boolean games with safety goals are presented next.

Propositional Safety Goals Let punishable(i) be a predicate that formalises when player i is punishable, that is if a trigger strategy can be constructed against i. For games with propositional safety goals the predicate punishable(i) reduces to: ∨v-i∈V-i ∧v′i ∈Vi (χ(v-i,v′i ) →¬ϕi ) is valid, for a propositional safety goal γi = Gϕi. We say that a player i of an iterated game is punishable when the predicate punishable(i) holds (and it is not punishable otherwise). We then have that:

Lemma 9 Let G = (N,Φ,Φ1, . . . ,Φn, γ1, . . . , γn) be an iterated Boolean game in which player i has a propositional safety goal γi =Gϕi. Then, if player i is not punishable, for all ⃗σ ∈ NE(G) we have that ρ(⃗σ) |= γi.

Proof sketch: W.l.o.g. assume that i = n and that player i is not punishable, that is, ∧v-i∈V-i ∨v′i ∈Vi (χ(v-i,v′i ) ∧ϕi ) is satisfiable. There is a function fn : V-n → Vn such that for each valuation ⃗v-n ∈ V-n we have ρ(⃗v-n, fn(⃗v-n)) |= ϕn. Consider an arbitrary ⃗σ ∈ NE(G), where σi = (Qi, q0i , δi, τi) for each player i. If ρ(⃗σ) satisfies Gϕi we are done. So assume ρ(⃗σ) ̸|= Gϕi. It now suffices to specify a strategy σ∗ n = (Q∗n , q00 n , δ∗ n , τ ∗ n ) for player n such that ρ(⃗σ-n, σ∗ n ) |= Gϕn. This is achieved by a product construction, in particular Q∗n = Q1 × · · · ×Qn-1 ×V, and the global behaviour of the profile ⃗σ-n against every possible behaviour of n is mimicked in the states of σ∗ n . Thus, for each time point t, the strategy σ∗ n can predict what ⃗v-i = ρ[t] ∩ (Φ \ Φi) will be and output an appropriate valuation f (⃗v-n) = v′i ensuring that (⃗v-n, v′n ) |= ϕn. Hence, we have that ρ(⃗σ-n, σ∗ n ) |= Gϕn, meaning that the strategy profile ⃗σ is not a pure Nash equilibrium.

Now we are in a position to prove a Folk Theorem for iterated Boolean games with propositional safety goals.

Theorem 10 Let G = (N,Φ,Φ1, . . . ,Φn, γ1, . . . , γn) be an iterated Boolean game in which each player i has a nontrivial propositional safety goal γi = Gϕi. Then, the following two statements are equivalent:

• (i) all players are punishable, and
• (ii) for all satisfiable ψ ∈ L, there is ⃗σ ∈ NE(G): ρ(⃗σ) |= ψ.

Proof sketch: For the direction from (i) to (ii) consider an arbitrary satisfiable formula ψ and assume all players to be punishable, that is, ∨v-i∈V-i ∧v′i ∈Vi (χ(v-i ,v′i ) → ¬ϕi) is valid for all players i. Then, by Lemma 1, there is some strategy profile ⃗σ such that ρ(⃗σ) |= ψ. Moreover, for every player j, there is some (v j1 , . . . , v j n ) ∈ V such that for all v′j ∈ Vj we have (v j1 , . . . , v j j-1 , v′j , v j j+1 , . . . , v j n ) ̸|= ϕj.

For every player i we build a machine strategy σ∗ i = (Q∗i , q0i , δ∗ i , τ ∗ i ) with Q∗i = (Q1 × · · · ×Qn) ∪ {q1i , . . . , q n i }, where each q j i is an additional state. These strategies are designed so that ρ(⃗σ∗ ) = ρ(⃗σ), that is, if all players play the strategy σ∗ i exhibits the same global behaviour as the equilibrium profile ⃗σ. Hence, ρ(⃗σ∗ ) |= ψ.

However, if (exactly) one player j adopts a strategy σ′ j such that ρ(⃗σ∗-j , σ′ j ) ̸= ρ(⃗σ∗ ), and let t be the earliest time point such that ρ(⃗σ∗-j , σ′ j )[t] ̸= ρ(⃗σ∗ )[t], then ⃗σ∗ is designed so that every player i distinct from j moves to state q j i and subsequently chooses v j i at t + 1. Thus, at t + 1 player j is punished in the sense that ϕj is not satisfied at t + 1 by ρ(⃗σ∗-j , σ′ j )[t +1]. It follows that ρ(⃗σ∗-j , σ′ j ) ̸|=Gϕj and that j cannot achieve his goal by deviating from ⃗σ∗ . We may conclude that ⃗σ∗ = (σ∗ 1 , . . . , σ∗ n ) ∈ NE(G).

For the direction from (ii) to (i) we prove the contrapositive. Assume that some player i is not punishable. As γi was assumed to be non-trivial, ¬γi is satisfiable. Yet, by Lemma 9, we have that ρ(⃗σ) |= γi for all equilibria ⃗σ |= γi. Hence, there is no ⃗σ ∈ NE(G) with ρ(σ) |= ¬γi.

As seen in Lemma 9 non-punishable players invariably achieve their goals in any Nash equilibrium. The next Folk Theorem, which is proved by using virtually the same constructions and arguments as in Theorem 10, refers to situations where non-punishable players have to be considered.

Theorem 11 Let G = (N,Φ,Φ1, . . . ,Φn, γ1, . . . , γn) be an iterated Boolean game in which each player i has a propositional safety goal γi ≡ Gϕi. Then, for all ψ ∈ L such that ψ ∧ ∧{γi : γi is not punishable} is satisfiable, there is a ⃗σ ∈ NE(G) such that ρ(⃗σ) |= ψ.

We can now leverage Theorem 10 and Theorem 11 so as to obtain PSPACE-completeness for the E-NASH problem for iterated Boolean games with propositional safety goals.

Proposition 12 The E-NASH and A-NASH problems for iterated Boolean games with propositional safety goals are PSPACE-complete.

Proof sketch: For membership in PSPACE, consider an arbitrary game G = (N, Φ, Φ1, . . . , Φn, γ1, . . . , γn) with propositional safety goals and an arbitrary ψ ∈ L. To decide whether ψ is sustained by some pure Nash equilibrium of G we proceed as follows.

1. N0 := ∅ 2. for i := 1 to n do 3. if ∀Φ \ Φi . ∃Φi . ϕ is true 4. then N0 := N0 ∪ {i} 5. else N0 := N0 6. end if 7. end-for 8. if ψ ∧ ∧i∈N0 γi is satisfiable then 9. return "yes" 10. else return "no" 11. end-if

In the for-loop, that is, in lines (1) through (7), this algorithm singles out the players that are not punishable. Checking the quantified Boolean formula ∀Φ \ Φi . ∃Φi . ϕ for truth is equivalent to checking ∧v-i∈V-i ∨v′i ∈Vi (χ(v-i,v′i ) ∧ ϕi) for satisfiability and can be achieved in Σp2 . Soundness of this step then follows from Lemma 9. In step (8) satisfiability of

ψ ∧ ∧i∈N0 γi is checked, which can be achieved in PSPACE. As PSPACE subsumes Σp2 , the algorithm runs in PSPACE.

For soundness and completeness, it now suffices to show that the following two statements are equivalent:

For the direction from (ii) to (i), assume that there is a ⃗σ ∈ NE(G) with ρ(⃗σ) |= ψ. By Lemma 9, it then follows that ρ(⃗σ) |= γi for all i ∈ N0. Hence, ψ ∧ ∧i∈N0 γi is satisfiable. The opposite direction is immediate by Theorem 11.

For PSPACE-hardness, we reduce the LTL satisfiability problem (which is known to be PSPACE-complete). Let ψ be an arbitrary LTL formula in L(Φ). We construct a game with two punishable players, both having propositional safety goals. The result then follows from Theorem 10.

General Safety Goals For general safety goals γi = Gϕi the predicate punishable(i) holds iff there is some LTL satisfiable formula χ ∈ L(Φ \ Φi) such that χ → ¬Gϕi is valid. Based on this definition the next Folk Theorem follows:

Theorem 13 Let G = (N,Φ,Φ1, . . . ,Φn, γ1, . . . , γn) be an iterated Boolean game where each player i has a non-trivial safety goal γi = Gϕi. Then, if all players are punishable, for all satisfiable ψ ∈ L, there is ⃗σ ∈ NE(G) with ρ(⃗σ) |= ψ.

Proof sketch: Assume that all players are punishable, that is, for each player i, there is some satisfiable χi ∈ L(Φ-i) such that χi → ¬Gϕi is valid. Moreover, let ψ ∈ L be a satisfiable formula. By Lemma 1 there is are strategy profiles ⃗σ(ψ), ⃗σ(χ1), . . . , ⃗σ(χn), the runs induced by which satisfy ψ and χ1 through χn, respectively. On their basis and by means of a product construction very similar to the one for Theorem 10, we can build for every player i a machine strategy σ∗ i = (Q∗i , q00 i , δ∗ i , τ ∗ i ) that incorporates a punishment strategy against every other player. It can then be shown that ρ(⃗σ∗ ) |= ψ and ⃗σ∗ ∈ NE(G).

6 Future work

In the model of iterated Boolean games we studied in this paper the players' goals are represented by LTL formulae. It is also natural to consider players whose behaviour, as motivated by their goals, would be better described by branchingtime temporal logics, such as CTL∗ [Emerson and Halpern, 1986] or the µ-calculus [Kozen, 1983]. Most probably a framework of this kind would lead to systems (games) with different computational complexity properties.

Another important technical component of this work was the formalisation of semantic conditions underpinning the Folk Theorems. Our study covered so-called (propositional) safety goals; other types of goals should be studied as well, for instance, goals with fairness or response properties.

We plan to analyse iterated Boolean games by means of other solution concepts. Punishment strategies arguably involve incredible threats. Subgame-perfect equilibrium seems to be appealing in this respect, as it does not suffer from this (alleged) defect and, moreover, Folk Theorems have been shown to hold for it (e.g., [Fudenberg and Maskin, 1986]).