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

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