**Thomas Troels Hildebrandt**

**February 2000**

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*.

BRICS WWW home page