Search

Spoiler-Duplicator games are used in finite model theory to examine the expressive power of logics. Their strategies have recently been reformulated as coKleisli maps of game comonads over relational structures, providing new results in finite model theory via categorical techniques. We present a novel framework for studying Spoiler-Duplicator games by viewing them as event structures. We introduce a first systematic method for constructing comonads for all one-sided Spoiler-Duplicator games: game comonads are now realised by adjunctions to a category of games, generically constructed from a comonad in a bicategory of game schema (called signature games). Maps of the constructed categories of games are strategies and generalise coKleisli maps of game comonads; in the case of one-sided games they are shown to coincide with suitably generalised homomorphisms. Finally, we provide characterisations of strategies on two-sided Spoiler-Duplicator games; in a common special case they coincide with spans of event structures., Comment: Extended version of the paper in Logic in Computer Science (LICS) 2024 Proceedings

Probabilistic concurrent/distributed strategies have so far not been investigated thoroughly in the context of imperfect information, where the Player has only partial knowledge of the moves made by the Opponent. In a situation where the Player and Opponent can make concurrent moves according to the game, and the Player cannot see the move of the Opponent, the move of the Player should be probabilistically independent of the move of the Opponent. What has been achieved is showing a bijection between strategies on a game with algebra and strategies on a regular (albeit more complex) game. We also succeeded in showing the results holds with neutral events. However it is still unclear if a well-formed bicategory of concurrent games with algebras can be defined. Our attempts to compose these strategies while managing the added structure didn't pan out. Concerning the other classic extensions of concurrent games the first results we presented show promise of a more general usage of games with algebra., Comment: 20 pages report as part of a master's degree internship

The article bridges between two major paradigms in computation, the functional, at basis computation from input to output, and the interactive, where computation reacts to its environment while underway. Central to any compositional theory of interaction is the dichotomy between a system and its environment. Concurrent games and strategies address the dichotomy in fine detail, very locally, in a distributed fashion, through distinctions between Player moves (events of the system) and Opponent moves (those of the environment). A functional approach has to handle the dichotomy much more ingeniously, through its blunter distinction between input and output. This has led to a variety of functional approaches, specialised to particular interactive demands. Through concurrent games we can more clearly see what separates and connects the differing paradigms, and show how: * to lift functions to strategies; the "Scott order" intrinsic to concurrent games plays a key role in turning functional dependency to causal dependency. * several paradigms of functional programming and logic arise naturally as subcategories of concurrent games, including stable domain theory; nondeterministic dataflow; geometry of interaction; the dialectica interpretation; lenses and optics; and their extensions to containers in dependent lenses and optics. * to transfer enrichments of strategies (such as to probabilistic, quantum or real-number computation) to functional cases.

Concurrent strategies based on event structures are examined from the viewpoint of 'may' and 'must' testing in traditional process calculi. In their pure form concurrent strategies fail to expose the deadlocks and divergences that can arise in their composition. This motivates an extension of the bicategory of concurrent strategies to treat the 'may' and 'must' behaviour of strategies under testing. One extension adjoins neutral moves to strategies but in so doing loses identities w.r.t. composition. This in turn motivates another extension in which concurrent strategies are accompanied by stopping configurations; the ensuing stopping strategies inherit the structure of a bicategory from that of strategies. The technical developments converge in providing characterisations of the 'may' and 'must' equivalences and preorders on strategies.

In the simplest form of event structure, a prime event structure, an event is associated with a unique causal history, its prime cause. However, it is quite common for an event to have disjunctive causes in that it can be enabled by any one of multiple sets of causes. Sometimes the sets of causes may be mutually exclusive, inconsistent one with another, and sometimes not, in which case they coexist consistently and constitute parallel causes of the event. The established model of general event structures can model parallel causes. On occasion however such a model abstracts too far away from the precise causal histories of events to be directly useful. For example, sometimes one needs to associate probabilities with different, possibly coexisting, causal histories of a common event. Ideally, the causal histories of a general event structure would correspond to the configurations of its causal unfolding to a prime event structure; and the causal unfolding would arise as a right adjoint to the embedding of prime in general event structures. But there is no such adjunction. However, a slight extension of prime event structures remedies this defect and provides a causal unfolding as a universal construction. Prime event structures are extended with an equivalence relation in order to dissociate the two roles, that of an event and its enabling; in effect, prime causes are labelled by a disjunctive event, an equivalence class of its prime causes. With this enrichment a suitable causal unfolding appears as a pseudo right adjoint. The adjunction relies critically on the central and subtle notion of extremal causal realisation as an embodiment of causal history. Finally, we explore subcategories which support parallel causes as well the key operations needed in developing probabilistic distributed strategies with parallel causes., Comment: arXiv admin note: text overlap with arXiv:1607.03747

We introduce the notion of a relative pseudomonad, which generalises the notion of a pseudomonad, and define the Kleisli bicategory associated to a relative pseudomonad. We then present an efficient method to define pseudomonas on the Kleisli bicategory of a relative pseudomonad. The results are applied to define several pseudomonads on the bicategory of profunctors in an homogeneous way, thus providing a uniform approach to the definition of bicategories that are of interest in operad theory, mathematical logic, and theoretical computer science., Comment: v3: Following referee comments: some material reorganised, presentation streamlined, definition of lax idempotent relative pseudomonad rephrased in terms of extensions. 32 pages. Accepted for publication in Selecta Mathematica (New Series)

In a distributed game we imagine a team Player engaging a team Opponent in a distributed fashion. Such games and their strategies have been formalised in concurrent games based on event structures. However there are limitations in founding strategies on traditional event structures. Sometimes a probabilistic distributed strategy relies on certain benign races where, intuitively, several members of team Player may race each other to make a common move. Although there are event structures which support such parallel causes, in which an event is enabled in several compatible ways, they do not support an operation of hiding central to the composition of strategies; nor do they support probability adequately. An extension of traditional event structures is devised which supports parallel causes and hiding, as well as the mix of probability and nondeterminism needed to account for probabilistic distributed strategies. The extension is tested in the construction of a bicategory of probabilistic distributed strategies with parallel causes. The bicategory is rich in operations relevant to probabilistic as well as deterministic parallel programming.

A summary of work on distributed games and strategies done within the first three years of the ERC project ECSYM is presented.

In 2011, Rideau and Winskel introduced concurrent games and strategies as event structures, generalizing prior work on causal formulations of games. In this paper we give a detailed, self-contained and slightly-updated account of the results of Rideau and Winskel: a notion of pre-strategy based on event structures; a characterisation of those pre-strategies (deemed strategies) which are preserved by composition with a copycat strategy; and the construction of a bicategory of these strategies. Furthermore, we prove that the corresponding category has a compact closed structure, and hence forms the basis for the semantics of concurrent higher-order computation.

We build a cartesian closed category, called Cho, based on event structures. It allows an interpretation of higher-order stateful concurrent programs that is refined and precise: on the one hand it is conservative with respect to standard Hyland-Ong games when interpreting purely functional programs as innocent strategies, while on the other hand it is much more expressive. The interpretation of programs constructs compositionally a representation of their execution that exhibits causal dependencies and remembers the points of non-deterministic branching.The construction is in two stages. First, we build a compact closed category Tcg. It is a variant of Rideau and Winskel's category CG, with the difference that games and strategies in Tcg are equipped with symmetry to express that certain events are essentially the same. This is analogous to the underlying category of AJM games enriching simple games with an equivalence relations on plays. Building on this category, we construct the cartesian closed category Cho as having as objects the standard arenas of Hyland-Ong games, with strategies, represented by certain events structures, playing on games with symmetry obtained as expanded forms of these arenas.To illustrate and give an operational light on these constructions, we interpret (a close variant of) Idealized Parallel Algol in Cho.

The aim of the workshop series Developments in Computational Models (DCM) is to bring together researchers who are currently developing new computational models or new features for traditional computational models, in order to foster their interaction, to provide a forum for presenting new ideas and work in progress, and to enable newcomers to learn about current activities in this area. The eighth workshop in the series, DCM 2012, was part of the celebrations of the Turing Centenary and was held as a satellite event of the Turing centenary conference Computability in Europe 2012 (CiE 2012) in Cambridge. It took place at Corpus Christi College in Cambridge on Sunday, 17 June 2013. This electronic proceedings volume includes one of the keynote papers as well as revised versions of papers accepted for presentation by the programme committee.

A compositional Petri net-based semantics is given to a simple language allowing pointer manipulation and parallelism. The model is then applied to give a notion of validity to the judgements made by concurrent separation logic that emphasizes the process-environment duality inherent in such rely-guarantee reasoning. Soundness of the rules of concurrent separation logic with respect to this definition of validity is shown. The independence information retained by the Petri net model is then exploited to characterize the independence of parallel processes enforced by the logic. This is shown to permit a refinement operation capable of changing the granularity of atomic actions.