# Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 1

Abstract : The dynamics of process calculi, e.g. CCS, have often been defined using a labelled transition system (LTS). More recently it has become common when defining dynamics to use reaction rules ---i.e. unlabelled transition rules--- together with a structural congruence. This form, which I call a reactive system, is highly expressive but is limited in an important way: LTSs lead more naturally to operational equivalences and preorders. This paper shows how to synthesise an LTS for a wide range of reactive systems. A label for an agent (process) 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 step. The key contribution of my work is the precise definition of `just large enough'' in terms of the categorical notion of relative pushout (RPO). I then prove that several operational equivalences and preorders (strong bisimulation, weak bisimulation, the traces preorder, and the failures preorder) are congruences when sufficient RPOs exist.
Keywords :
Document type :
Reports
Domain :
Complete list of metadatas

Cited literature [4 references]

https://hal.inria.fr/inria-00072194
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 8:02:49 PM
Last modification on : Friday, May 25, 2018 - 12:02:03 PM
Document(s) archivé(s) le : Sunday, April 4, 2010 - 10:57:52 PM

### Identifiers

• HAL Id : inria-00072194, version 1

### Citation

James J. Leifer. Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 1. [Research Report] RR-4394, INRIA. 2002. ⟨inria-00072194⟩

Record views