Observational trees as models for concurrency

Abstract

Given an automaton, its behaviour can be modelled as the sets of strings over an alphabet A that can be accepted from any of its states. When considering concurrent systems, we can see a concurrent agent as an automaton, where non-determinism derives from the fact that its states can offer a different behaviour at different moments in time. Non-deterministic computations between a pair of states can then no longer be described as a ‘set’ of strings in a free monoid. Consequently, between two states we will have a labelled structured set of computations, where the structure describes the possibility of two computations parting from each other while maintaining the same observable steps. In this paper, we shall consider different kinds of observation domains and related structured sets of computations. Structured sets of computations will be organised as a category of generalised trees built over a meet-semilattice monoid formalizing the observation domain. Theorems allowing us to introduce the usual concurrency operators in the models and relating different models will then be obtained by first considering ordinary functors (on and between the observation domains), and then lifting them to the categories of structured sets of computations.