zbMATH — the first resource for mathematics

Deriving bisimulation congruences for reactive systems. (English) Zbl 0999.68141
Palamidessi, Catuscia (ed.), CONCUR 2000 - Concurrency theory. 11th international conference, University Park, PA, USA, August 22-25, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1877, 243-258 (2000).
Summary: The dynamics of reactive systems, e.g. CCS, has often been defined using a labelled transition system (LTS). More recently it has become natural in defining dynamics to use reaction rules – i.e. unlabelled transition rules – together with a structural congruence. But LTSs lead more naturally to behavioural equivalences. So one would like to derive from reaction rules a suitable LTS. This paper shows how to derive an LTS for a wide range of reactive systems. A label for an agent $$a$$ is defined to be any context $$F$$ which intuitively is just large enough so that the agent $$Fa$$ (“$$a$$ in context $$F$$”) is able to perform a reaction. The key contribution of this paper is a precise definition of “just large enough”, in terms of the categorical notion of relative pushout (RPO), which ensures that bisimilarity is a congruence when sufficient RPOs exist. Two examples – a simplified form of action calculi and term-rewriting – are given, for which it is shown that sufficient RPOs indeed exist. The thrust of this paper is, therefore, towards a general method for achieving useful behavioural congruence relations.
For the entire collection see [Zbl 0944.00069].

MSC:
 68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)