Categorical Models for Concurrency: Independence, Fairness and Dataflow

Thomas Troels Hildebrandt

February 2000

Abstract:

This thesis is concerned with formal semantics and models for concurrent computational systems, that is, systems consisting of a number of parallel computing sequential systems, interacting with each other and the environment. A formal semantics gives meaning to computational systems by describing their behaviour in a mathematical model. For concurrent systems the interesting aspect of their computation is often how they interact with the environment during a computation and not in which state they terminate, indeed they may not be intended to terminate at all. For this reason they are often referred to as reactive systems, to distinguish them from traditional calculational systems, as e.g. a program calculating your income tax, for which the interesting behaviour is the answer it gives when (or if) it terminates, in other words the (possibly partial) function it computes between input and output. Church's thesis tells us that regardless of whether we choose the lambda calculus, Turing machines, or almost any modern programming language such as C or Java to describe calculational systems, we are able to describe exactly the same class of functions. However, there is no agreement on observable behaviour for concurrent reactive systems, and consequently there is no correspondent to Church's thesis. A result of this fact is that an overwhelming number of different and often competing notions of observable behaviours, primitive operations, languages and mathematical models for describing their semantics, have been proposed in the litterature on concurrency.

The work presented in this thesis contributes to a categorical approach to semantics for concurrency which have been developed through the last 15 years, aiming at a more coherent theory. The initial stage of this approach is reported on in the chapter on models for concurrency by Winskel and Nielsen in the Handbook of Logic in Computer Science, and focuses on relating the already existing models and techniques for reasoning about them. This work was followed by a uniform characterisation of behavioural equivalences from the notion of bisimulation from open maps proposed by Joyal, Winskel and Nielsen, which was applicable to any of the categorical models and shown to capture a large number of existing variations on bisimulation. At the same time, a class of abstract models for concurrency was proposed, the presheaf models for concurrency, which have been developed over the last 5 years, culminating in the recent thesis of Cattani.

This thesis treats three main topics in concurrency theory: independence, fairness and non-deterministic dataflow.

Our work on independence, concerned with explicitly representing that actions result from independent parts of a system, falls in two parts. The first contributes to the initial work on describing formal relationships between existing models. The second contributes to the study of concrete instances of the abstract notion of bisimulation from open maps. In more detail, the first part gives a complete formal characterisation of the relationship between two models, transition systems with independence and labelled asynchronous transition systems respectively, which somehow escaped previous treatments. The second part studies the borderline between two well known notions of bisimulation for independence models such as 1-safe Petri nets and the two models mentioned above. The first is known as the history-preserving bisimulation (HPB), the second is the bisimulation obtained from the open maps approach, originally introduced under the name hereditary history-preserving bisimulation (HHPB) as a strengthening of HPB obtained by adding backtracking. Remarkably, HHPB has recently been shown to be undecidable for finite state systems, as opposed to HPB which is known to be decidable. We consider history-preserving bisimulation with bounded backtracking, and show that it gives rise to an infinite, strict hierarchy of decidable history-preserving bisimulations seperating HPB and HHPB.

The work on fairness and non-deterministic dataflow takes its starting point in the work on presheaf models for concurrency in which these two aspects have not been treated previously.

Fairness is concerned with ruling out some completed, possibly infinite, computations as unfair. Our approach is to give a presheaf model for the observation of infinite as well as finite computations. This includes a novel use of a Grothendieck topology to capture unique completions of infinite computations. The presheaf model is given a concrete representation as a category of generalised synchronisation trees, which we formally relate to the general transition systems proposed by Hennessy and Stirling for the study of fairness. In particular the bisimulation obtained from open maps is shown to coincide with their notion of extended bisimulation. Benefitting from the general results on presheaf models we give the first denotational semantics of Milners SCCS with finite delay that coincides with his operational semantics up to extended bisimulation.

The work on non-deterministic dataflow, i.e. systems communicating assynchronously via buffered channels, recasts dataflow in a modern categorical light using profunctors as a generalisation of relations. The well known causal anomalies associated with relational semantics of indeterminate dataflow are avoided, but still we preserve much of the intuitions of a relational model. The model extends the traditional presheaf models usually applied to semantics for synchronous communicating processes described by CCS-like calculi, and thus opens up for the possibility of combining these two paradigms. We give a concrete representation of our model as a category of (unfolded) monotone port automata, previously studied by Panangaden and Stark. We show that the notion of bisimulation obtained from open maps is a congruence with respect to the operations of dataflow. Finally, we use the categorical formulation of feedback using traced monoidal categories. A pay off is that we get a semantics of higher-order networks almost for free, using the geometry of interaction construction.

Available as PostScript, PDF.