Deterministic concurrent strategies
Glynn Winskel · Formal Aspects of Computing · 2012
Abstract Nondeterministic concurrent strategies—those strategies compatible with copy-cat behaving as identity w.r.t. composition—have been characterised as certain maps of event structures. This leads to a bicategory of general concurrent games in which the maps are nondeterministic concurrent strategies. This paper explores the important sub-bicategory of deterministic concurrent strategies. It is shown that deterministic strategies in a game can be identified with certain subgames, with the benefit that the bicategory of deterministic games becomes equivalent to a technically-simpler order-enriched category. Via a characterisation, deterministic strategies are shown to coincide with the receptive ingenuous strategies of Melliès and Mimram. Deterministic strategies determine closure operators , in accord with an early definition of Abramsky and Melliès. Known subcategories appear as special cases: Berry’s order-enriched category of dI-domains and stable functions arises as a full subcategory in which the games comprise solely of Player moves; the `simple games’ of Hyland et al., a basis for much of game semantics, form a subcategory in which the games permit no concurrency, Player-Opponent moves alternate and Opponent always moves first.