Search

Abstract: We consider nondeterministic concurrent games played on event structures and study their determinacy problem—the existence of winning strategies. It is known that when the winning conditions of the games are characterised by a collection of finite winning sets/plays, a restriction (called race-freedom) on the boards where the games are played guarantees determinacy. However the games may no longer be determined when the winning sets are infinite. This paper provides a study of concurrent games and nondeterministic winning strategies by analysing conditions that ensure determinacy when infinitely many events are played, that is, when the winning sets are infinite. The main result is a determinacy theorem for a class of games with a bounded concurrency property and infinite winning sets shown to be finitely decidable. [Copyright &y& Elsevier]

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. [ABSTRACT FROM AUTHOR]

The article discusses causal models, such as Petri nets and event structures, how they have been rediscovered in a wide variety of recent applications and why they are fundamental to computer science. A discussion of their present limitations leads to their extension with symmetry. The consequences, actual and potential, are discussed. [ABSTRACT FROM AUTHOR]

Abstract: A prime algebraic lattice can be characterised as isomorphic to the downwards-closed subsets, ordered by inclusion, of its complete primes. It is easily seen that the downwards-closed subsets of a partial order form a completely distributive algebraic lattice when ordered by inclusion. The converse also holds; any completely distributive algebraic lattice is isomorphic to such a set of downwards-closed subsets of a partial order. The partial order can be recovered from the lattice as the order of the lattice restricted to its complete primes. Consequently prime algebraic lattices are precisely the completely distributive algebraic lattices. The result extends to Scott domains. Several consequences are explored briefly: the representation of Berry’s dI-domains by event structures; a simplified form of information systems for completely distributive Scott domains; and a simple domain theory for concurrency. [Copyright &y& Elsevier]

A simple domain theory for concurrency is presented. Based on a categorical model of linear logic and associated comonads, it highlights the role of linearity in concurrent computation. Two choices of comonad yield two expressive metalanguages for higher-order processes, both arising from canonical constructions in the model. Their denotational semantics are fully abstract with respect to contextual equivalence. One language derives from an exponential of linear logic; it supports a straightforward operational semantics with simple proofs of soundness and adequacy. The other choice of comonad yields a model of affine-linear logic, and a process language with a tensor operation to be understood as a parallel composition of independent processes. The domain theory can be generalised to presheaf models, providing a more refined treatment of nondeterministic branching. The article concludes with a discussion of a broader programme of research, towards a fully fledged domain theory for concurrency. [Copyright &y& Elsevier]

The aim of this paper is to harness the mathematical machinery around presheaves for the purposes of process calculi. Joyal, Nielsen and Winskel proposed a general definition of bisimulation from open maps. Here we show that open-map bisimulations within a range of presheaf models are congruences for a general process language, in which CCS and related languages are easily encoded. The results are then transferred to traditional models for processes. By first establishing the congruence results for presheaf models, abstract, general proofs of congruence properties can be provided and the awkwardness caused through traditional models not always possessing the cartesian liftings, used in the breakdown of process operations, are side stepped. The abstract results are applied to show that hereditary history-preserving bisimulation is a congruence for CCS-like languages to which is added a refinement operator on event structures as proposed by van Glabbeek and Goltz. [Copyright &y& Elsevier]

Abstract: This paper studies how to adjoin probability to event structures, leading to the model of probabilistic event structures. In their simplest form, probabilistic choice is localised to cells, where conflict arises; in which case probabilistic independence coincides with causal independence. An event structure is associated with a domain—that of its configurations ordered by inclusion. In domain theory, probabilistic processes are denoted by continuous valuations on a domain. A key result of this paper is a representation theorem showing how continuous valuations on the domain of a confusion-free event structure correspond to the probabilistic event structures it supports. We explore how to extend probability to event structures which are not confusion-free via two notions of probabilistic runs of a general event structure. Finally, we show how probabilistic correlation and probabilistic event structures with confusion can arise from event structures which are originally confusion-free by using morphisms to rename and hide events. [Copyright &y& Elsevier]