A BRICS Mini-Course
October 3 and 4, 1996
Lectures by
Vladimiro Sassone
Dipartimento di Informatica, Pisa, Italy
The operational semantics of concurrent systems is often specified by means of labelled transition systems. These simple structures provide a level of abstraction which is appropriate for many applications, and allow us to take an ``extensional'' view by focusing on the labels, meant to represent the system's observable behaviour. They are, however, so-called interleaving models, meaning that they fail to draw natural distinctions between interleaved and concurrent execution of actions, so losing track of the casual dependencies between them.
Many authors have recently argued in favour of generalising transition systems, aiming at transition-based models in which the concurrent activity of several agents is explicitly represented by ``higher dimensional'' transitions. Besides any consideration about the semantic relevance of cause/effect relationships, such non-interleaving models can be helpful in more pragmatic tasks, such as model checking, where they can reduce considerably the state-space explosion problem.
We focus on a very recent model-actually still under development-which provides an elementary, set-theoretic formalisation of the idea of higher dimensional transition: the Higher Dimensional Transition Systems (HDTS). First, we review some of the proposals in the literature and compare them to HDTS, trying to show that they are rather natural structures. Then, we develop an extensional semantic theory for HDTS centered on a notion of history-preserving bisimulation that can be formulated abstractly in the ``bisimulation-via-open-maps'' paradigm. We conclude by presenting some of the latest developments, as well as open problems and directions for further research, aiming at demonstrating that HDTS are interesting mathematical structures, besides being a rather general model of concurrency.