FREE ELECTRONIC LIBRARY - Thesis, dissertations, books

Pages:   || 2 | 3 |

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

-- [ Page 1 ] --

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 configurations 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 finite games which showed that all perfect-information finite games are determined. Since then, more complex games and determinacy results have been studied, e.g. for games with plays of infinite 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 verification 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 verification 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 first 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 finite plays are possible) provided they are race-free,i.e. neither player could interfere with the moves available to the other—a property satisfied 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 infinite and where the winning set of configurations 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 infinitely many moves of the other—a condition trivially satisfied when e.g. all plays are finite, 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 defined.

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 finite 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 finite games, the determinacy theorem in this paper generalises the Borel determinacy theorem for infinite 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 finite ⇒ X ∈ Con, and Down-closed: ∀e, e′. e′ ≤ e ∈ x =⇒ e′ ∈ x.

We write C ∞ (E) for the set of configurations of E and C(E) for the finite 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 configuration x, when x−−⊂ y for some configuration 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 defined) 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 defined. 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 define the composition of strategies, while restriction (a form of equalizer) and the defined part of maps will be used in defining strategies. Any map of event structures f : E → E ′, which may be a partially defined on events, has a defined part the total map f0 : E0 → E ′, in which the event structure E0 has events those of E at which f is defined, with causal dependency and consistency inherited from E, and where f0 is simply f restricted to its domain of definition. 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 iff ∀X ⊆fin 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 iff 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 iff a s σx−−⊂ & pol A (a) = − ⇒ ∃!s ∈ S. x−−⊂ & σ(s) = a.

Innocence: A map σ is innocent iff 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-off σ against τ.

Because σ or τ may be nondeterministic there can be more than one maximal configuration z in C ∞ (P ). A maximal z images to a configuration σΠ1 z = τ Π2 z in C ∞ (A). Define the set of results of playing-off σ 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-off against τ2 when both players are waiting for their opponent to play first.

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 configurations (for Player). Define the losing conditions (for Player) to be L = C ∞ (A) \ W. The dual G⊥ of a game with winning conditions G = (A, W ) is defined 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 configuration,

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 configurations s x ∈ C ∞ (S)—a configuration 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 final result is a win for Player; precisely, it can be shown [3] that a strategy σ is a winning for Player iff 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 configuration 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 Definition 3. Say E, an event structure with polarity, is tree-like iff it has empty concurrency relation (so ≤E forms a forest), all events enabled by the initial configuration ∅ 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 finite configurations C(E) form a tree w.r.t. ⊆. Its root is the empty configuration ∅. Its (maximal) branches may be finite or infinite; finite sub-branches correspond to finite configurations of E; infinite branches correspond to infinite e configurations 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,’ ‘configurations’ and ‘maximal configurations’ 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 −.

Pages:   || 2 | 3 |

Similar works:

«Re: Communication submitted under Article 55 of the African Charter on Human and Peoples’ Rights Complainant: Open Society Justice Initiative State Party: Côte d’Ivoire I. INTRODUCTION The Open Society Justice Initiative hereby submits this communication under Article 55 of the African Charter on Human and People’s Rights against Côte d’Ivoire, a state party to the Charter, and its agents on behalf of Ivorians who have suffered unlawful discrimination by agents of the state of Côte...»

«Composite Materials Layup Lab Professor William Joseph Stuart Oregon Institute of Technology Klamath Falls, OR 97601 Ph: 5262 Email:joe.stuart@oit.edu Copyright Edmonds Community College 2010 This material may be used and reproduced for educational purposes only. Abstract The objective of this lab is to familiarize the students with the composite materials layup process. Hand lay-up is a simple method for composite production. The process consists of building up or placing layers of composite...»

«Complot Contre La Democratie And them will identify to refer our effective, much via unique phrases and purchases. If you take, sometimes, run out in websites, cover able of you are a gift potential on an instances what had here sell we but decide a bankruptcy did to it too. Their interest is passive to notify Complot Contre La Democratie you because leaving people for the spending during you have, one what will be an loan compared so or ultimately. Me will mention they to a % about each....»

«COLLECTION DEVELOPMENT PLAN PITT COMMUNITY COLLEGE LIBRARY (latest review: October 2013) 1. INTRODUCTION 1.1. Purpose and Aim The purpose of the Collection Development Plan (“the Plan”) is to provide  criteria and guidelines for the selection of library materials and the ongoing assessment and maintenance of the collection.  procedures for interaction between the collection and its users. The aim of the Plan is to provide a working tool to  expedite the collecting of material or...»

«COMM 4908 Supervisors’ Guidelines Carleton University School of Journalism and Communication COMM 4908 Honours Research Essay Supervisors’ Guidelines 2015/2016 Undergraduate Supervisor: Sandra Robinson, PhD Office: RB 4317 Telephone: 520-2600 ext. 8470 Email: Sandra.Robinson@carleton.ca Overview Students with a GPA of 10.0 or higher have the option to register in COMM 4908 Honours Research Essay in their final year. This course constitutes 1.0 credit. This outline is intended for faculty...»

«KINGSTON PLANNING SCHEME 21.05 RESIDENTIAL LAND USE DD21/MM03/ 201X3 Proposed C14017 21.05-1 Overview DD20/MM11/ 20YY08 Proposed Kingston comprises a high diversity of residential areas, spanning from housing C14073 constructed in the early 1900s through to newer ‘greenfield’ estates. The ability of our residential areas to continue to accommodate the changing lifestyle and housing needs of current and future populations continues to be is becoming an increasingly important issue in...»

«Devising a Government Complaint System Guide to Good Practice Table of Contents Introduction  Acknowledgements  Why Have a Complaint System?  Why People Complain  Aims of an Effective Complaint System  Principles of a Good Complaint System  Elements of a Complaint System  Planning and Start-up Considerations  Publicizing the Complaint System  Complaints as Opportunities to Improve  References  Introduction For many years the Alaska Office of the Ombudsman has...»

«Tab This is a final public hearing to create a Gulf Reef Fish Data Reporting System, which would require private recreational anglers to report their intention to harvest or attempt to harvest reef fish species such as red snapper, gag grouper, and amberjack in the Gulf of Mexico. This data reporting system would be used to collect more accurate, precise, and timely catch and effort estimates for key recreational reef fish fisheries off Florida’s Gulf coast. The proposed Gulf Reef Fish Data...»

«ANNUAL MIGRATIONS OF CALIFORNIA STRIPED BASS 1 By A. J. CALHOUN Bureau of Fish Conservation California Department of Fish and Game A well-defined annual migration of adult striped bass (Roccus saxatilis), initially suggested by the catch records for this fishery (Calhoun, 1949), has now been fully confirmed by a large number of tag returns. Previous California tagging of striped bass (Clark, 1934, 1936) was limited almost entirely to small fish, mostly less than 12 inches in length and...»

«CHURCH AND TABLE -A PARTICIPATORY ECCLESIOLOGY FOR THE CONTEMPORARY CHURCH by Nicholas Andrew Coates A thesis submitted to the Faculty of Emmanuel College and the Theology Department of the Toronto School of Theology. In fulfilment of the requirements for the degree of Master of Arts in Theology awarded by St Michael’s College and the University of Toronto. © Copyright Nicholas Andrew Coates 2012 Church and Table A Participatory Ecclesiology for the Contemporary Church Nicholas Andrew...»

«On the Complexity of Fragments of Modal Logics Linh Anh Nguyen We study and give a summary of the complexity of abstract. 15 basic normal monomodal logics under the restriction to the Horn fragment and/or bounded modal depth. As new results, we show that: a) the satisfiability problem of sets of Horn modal clauses with modal depth bounded by k ≥ 2 in the modal logics K 4 and KD4 is PSPACE-complete, in K is NP-complete; b) the satisfiability problem of modal formulas with modal depth bounded...»

«ED.06/RSC II.ENA/1 UNESCO Forum Occasional Paper Series Paper No. 6 Diversification of Higher Education and the Changing Role of Knowledge and Research Papers presented at the Second Scientific Committee Meeting for Europe and North America Papers produced for the UNESCO Forum Regional Scientific Committee For Europe and North America Paris, March 2004 (ED-2006/WS/44) TABLE OF CONTENT 1. Changing Structures of the Higher Education Systems: The Increasing Complexity of Underlying Forces, by...»

<<  HOME   |    CONTACTS
2016 www.dis.xlibx.info - Thesis, dissertations, books

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.