# «Abstract. Just as traditional games can be represented by trees, so concurrent games can be represented by event structures. We show the determinacy ...»

Borel Determinacy of Concurrent Games

Julian Gutierrez1 and Glynn Winskel2

University of Oxford, Computer Science Department, Oxford, UK.

University of Cambridge, Computer Laboratory, Cambridge, UK.

Abstract. Just as traditional games can be represented by trees, so

concurrent games can be represented by event structures. We show the

determinacy of such concurrent games with Borel sets of conﬁgurations as

winning conditions, provided they are race-free and bounded-concurrent.

Both properties are shown necessary. The determinacy proof proceeds via a reduction to the determinacy of tree games, and the determinacy of these in turn reduces to the determinacy of Gale-Stewart games.

1 Introduction In logic the study of determinacy in games (the existence of a winning strategy or counter-strategy) dates back, at least, to Zermelo’s work [12] on ﬁnite games which showed that all perfect-information ﬁnite games are determined. Since then, more complex games and determinacy results have been studied, e.g. for games with plays of inﬁnite length. A research line that began in the 1950s with the seminal work of Gale and Stewart [5] on open games culminated with the work of Martin [6] who showed that two-player zero-sum sequential games with perfect information in which the winning conditions were Borel are determined.

In computer science determinacy results have most often been used rather than investigated. Frequently decision and veriﬁcation problems are represented by games with winning conditions where winning strategies encode solutions to the problems being represented by the games. The determinacy of games ensures that in all cases there is a solution to the decision or veriﬁcation problem under consideration, so is a computationally desirable property.

A common feature of the games mentioned above is that they are generally represented as trees. As a consequence, the plays of such games form total orders—the branches. The games we consider in this paper are not restricted to games represented by trees. Instead, they are played on games represented by event structures. Event structures [9] are the concurrency analogue of trees. Just as transitions systems unfold to trees, so Petri nets and asynchronous transition systems unfold to event structures. Plays are now partial orders of moves.

The concurrent games we consider are an extension of those introduced in [10]. Games there can be thought of as highly-interactive, distributed games between Player (thought of as a team of players) and Opponent (a team of opponents). The games model, as ﬁrst introduced in [10], was extended with winning conditions in [3]. There a determinacy result was given for well-founded games 2 J. Gutierrez, G. Winskel (i.e. where only ﬁnite plays are possible) provided they are race-free,i.e. neither player could interfere with the moves available to the other—a property satisﬁed by all best-known games on trees/graphs, both sequential and concurrent.

Here we extend the main result of [3] by providing a much more general determinacy theorem. We consider concurrent games in which plays may be inﬁnite and where the winning set of conﬁgurations forms a Borel set.

In particular we show that such games are determined provided that they are race-free and satisfy a structural condition we call bounded concurrency. Bounded concurrency expresses that no move of one of the players can be concurrent with inﬁnitely many moves of the other—a condition trivially satisﬁed when e.g. all plays are ﬁnite, the games are sequential, or the games have rounds where simple choices are made (usual in traditional concurrent games). Bounded concurrency and race-freedom hold implicitly in games as traditionally deﬁned.

We also show in what sense both bounded concurrency and race-freedom are necessary for Borel determinacy. Our determinacy proof follows by a reduction to the determinacy of Borel games, shown by Martin [6].

Related Work Determinacy problems have been studied for more than a century: for ﬁnite games [12]; open games [5]; Borel games [6]; or Blackwell games [7], to mention a few particularly relevant to concurrency and computer science.

Whereas the determinacy theorem in [3] is a concurrent generalisation of Zermelo’s determinacy theorem for ﬁnite games, the determinacy theorem in this paper generalises the Borel determinacy theorem for inﬁnite games from trees to event structures, so from total orders to partial orders of moves.

The results here apply to zero-sum concurrent games with perfect information. The games here require additional structure in order to model imperfect information [4] or stochastic features, so the determinacy result here does not apply directly to Blackwell games [7], the imperfect-information concurrent games played on graphs in [2] or the nonzero-sum concurrent games of [1].

Structure of the Paper In Section 2 we present concurrent games represented as event structures. Section 3 introduces tree and Gale-Stewart games as variants of concurrent games. In Section 4 race-freedom and bounded concurrency are studied. Section 5 contains the determinacy theorem, preceding the conclusion.

Consistent: ∀X ⊆ x. X is ﬁnite ⇒ X ∈ Con, and Down-closed: ∀e, e′. e′ ≤ e ∈ x =⇒ e′ ∈ x.

We write C ∞ (E) for the set of conﬁgurations of E and C(E) for the ﬁnite congurations. Two events e1, e2 which are both consistent and incomparable with respect to causal dependency in an event structure are regarded as concurrent, e′, meaning written e1 co e2. In games the relation of immediate dependency e ′ ′ e and e are distinct with e ≤ e and no event in between plays an important role. For X ⊆ E we write [X] for {e ∈ E | ∃e′ ∈ X. e ≤ e′ }, the down-closure of X; note if X ∈ Con then [X] ∈ Con. We use x−⊂y to mean y covers x in e C ∞ (E), i.e., x ⊂ y with nothing in between, and x−−⊂ y to mean x ∪ {e} = y for e x, y ∈ C ∞ (E) and event e ∈ x. We use x−−⊂, expressing that event e is enabled / e at conﬁguration x, when x−−⊂ y for some conﬁguration y.

Let E and E ′ be event structures. A map of event structures is a partial function on events f : E → E ′ such that for all x ∈ C(E) its direct image f x ∈ C(E ′ ) and if e1, e2 ∈ x and f (e1 ) = f (e2 ) (with both deﬁned) then e1 = e2. The map expresses how the occurrence of an event e in E induces the coincident occurrence of the event f (e) in E ′ whenever it is deﬁned. Maps of event structures compose as partial functions, with identity maps given by identity functions. We say that the map is total if the function f is total. Say a total map of event structures is rigid when it preserves causal dependency.

The category of event structures is rich in useful constructions on processes.

In particular, pullbacks are used to deﬁne the composition of strategies, while restriction (a form of equalizer) and the deﬁned part of maps will be used in deﬁning strategies. Any map of event structures f : E → E ′, which may be a partially deﬁned on events, has a deﬁned part the total map f0 : E0 → E ′, in which the event structure E0 has events those of E at which f is deﬁned, with causal dependency and consistency inherited from E, and where f0 is simply f restricted to its domain of deﬁnition. Given an event structure E and a subset R ⊆ E of its events, the restriction E ↾R is the event structure comprising events {e ∈ E | [e] ⊆ R} with causal dependency and consistency inherited from E; we sometimes write E \ S for E ↾ (E \ S), where S ⊆ E.

Event Structures with Polarity Both a game and a strategy in a game are represented with event structures with polarity, comprising an event structure E together with a polarity function pol : E → {+, −} ascribing a polarity + (Player) or − (Opponent) to its events; the events correspond to moves. Maps of event structures with polarity, are maps of event structures which preserve polarities. An event structure with polarity E is deterministic iﬀ ∀X ⊆ﬁn E. Neg[X] ∈ ConE =⇒ X ∈ ConE, where Neg[X] =def {e′ ∈ E | pol (e′ ) = − & ∃e ∈ X. e′ ≤ e}. We write P os[X] if pol(e′ ) = +. The dual, E ⊥, of an event structure with polarity E comprises the same underlying event structure E but with a reversal of polarities.

Given two sets of events x and y, we write x ⊂+ y to express that x ⊂ y and pol (y \ x) = {+}; similarly, we write x ⊂− y iﬀ x ⊂ y and pol (y \ x) = {−}.

4 J. Gutierrez, G. Winskel Games and Strategies Let A be an event structure with polarity—a game;

its events stand for the possible moves of Player and Opponent and its causal dependency and consistency relations the constraints imposed by the game.

A strategy (for Player) in A is a total map σ : S → A from an event structure with polarity S, which is both receptive and innocent. Receptivity ensures an openness to all possible moves of Opponent. Innocence, on the other hand, restricts the behaviour of Player; Player may only introduce new relations of immediate causality of the form ⊖ ⊕ beyond those imposed by the game.

Receptivity: A map σ is receptive iﬀ a s σx−−⊂ & pol A (a) = − ⇒ ∃!s ∈ S. x−−⊂ & σ(s) = a.

Innocence: A map σ is innocent iﬀ s′ & (pol (s) = + or pol (s′ ) = −) then σ(s) σ(s′ ).

s Say a strategy σ : S → A is deterministic if S is deterministic.

The event structure P describes the play resulting from playing-oﬀ σ against τ.

Because σ or τ may be nondeterministic there can be more than one maximal conﬁguration z in C ∞ (P ). A maximal z images to a conﬁguration σΠ1 z = τ Π2 z in C ∞ (A). Deﬁne the set of results of playing-oﬀ σ against τ to be

Note that Player (or Opponent) can try to force some play to happen sequentially by adding causal dependencies, e.g. when using strategy σ2 (or τ2 ). This situation may lead to a deadlock as with σ2 played-oﬀ against τ2 when both players are waiting for their opponent to play ﬁrst.

Determinacy and Winning Conditions A game with winning conditions [3] comprises G = (A, W ) where A is an event structure with polarity and the set W ⊆ C ∞ (A) consists of the winning conﬁgurations (for Player). Deﬁne the losing conditions (for Player) to be L = C ∞ (A) \ W. The dual G⊥ of a game with winning conditions G = (A, W ) is deﬁned to be G⊥ = (A⊥, L), a game where the roles of Player and Opponent are reversed, as are correspondingly the roles of winning and losing conditions.

A strategy in G is a strategy in A. A strategy in G is regarded as winning if it always prescribes moves for Player to end up in a winning conﬁguration,

**no matter what the activity or inactivity of Opponent. Formally, a strategy σ :**

S → A in G is winning (for Player) if σx ∈ W for all ⊕-maximal conﬁgurations s x ∈ C ∞ (S)—a conﬁguration x is ⊕-maximal if whenever x−−⊂ then the event s has −ve polarity. Equivalently, a strategy σ for Player is winning if when played against any counter-strategy τ of Opponent, the ﬁnal result is a win for Player; precisely, it can be shown [3] that a strategy σ is a winning for Player iﬀ all the results σ, τ lie within W, for any counter-strategy τ of Opponent.

Sometimes we say a strategy σ dominates a counter-strategy τ (and vice versa) when σ, τ ⊆ W (respectively, σ, τ ⊆ L). A game with winning conditions is determined when either Player or Opponent has a winning strategy in the game.

** Example 2. Consider the game A with two inconsistent events ⊕ and ⊖ with the obvious polarities and winning conditions W = {{⊕}}.**

The game (A, W ) is not determined: no strategy of either player dominates all counter-strategies of the other player. Any strategy σ : S → A cannot be winning as it must by receptivity have ⊖ → ⊖, so a ⊕-maximal conﬁguration of S with image {⊖} ∈ W. By a / symmetric argument no counter-strategy for Opponent can be winning.

**3 Tree Games and Gale–Stewart Games**

We introduce tree games as a special case of concurrent games, traditional Gale– Stewart games as a variant, and show how to reduce the determinacy of tree games to that of Gale–Stewart games. Via Martin’s theorem for the determinacy of Gale–Stewart games with Borel winning conditions we show that tree games with Borel winning conditions are determined.

3.1 Tree Games Deﬁnition 3. Say E, an event structure with polarity, is tree-like iﬀ it has empty concurrency relation (so ≤E forms a forest), all events enabled by the initial conﬁguration ∅ have the same polarity, and is such that polarities alternate 6 J. Gutierrez, G. Winskel e′ then pol E (e) = pol E (e′ ). A tree game is (E, W ), a along branches, i.e. if e concurrent game with winning conditions in which E is tree-like.

Proposition 4. Let E be a tree-like event structure with polarity. Then, its ﬁnite conﬁgurations C(E) form a tree w.r.t. ⊆. Its root is the empty conﬁguration ∅. Its (maximal) branches may be ﬁnite or inﬁnite; ﬁnite sub-branches correspond to ﬁnite conﬁgurations of E; inﬁnite branches correspond to inﬁnite e conﬁgurations of E. Its arcs, associated with x−−⊂ x′, are in 1-1 correspondence e with events e ∈ E. The events e associated with initial arcs ∅−−⊂ x all have the same polarity. In a branch ei+1 e1 e2 e3 ei ∅−−⊂ x1 −−⊂ x2 −−⊂ · · · −−⊂ xi −−⊂ · · · the polarities of the events e1, e2,..., ei,... alternate.

Proposition 4 gives the precise sense in which the terms ‘arc,’ ‘sub-branch’ and ‘branch’ are synonyms for the terms ‘events,’ ‘conﬁgurations’ and ‘maximal conﬁgurations’ when an event structure with polarity is tree-like. Notice that for a non-empty tree-like event structure with polarity, all the events that can occur initially share the same polarity. We say a non-empty tree game (E, W ) has polarity + or − depending on whether its initial events are +ve (positive) or −ve (negative). We adopt the convention that the empty game (∅, ∅) has polarity +, and the empty game (∅, {∅}) has polarity −.