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.
Document type :
Reports
Complete list of metadatas

Cited literature [4 references]  Display  Hide  Download

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
Long-term archiving on : Sunday, April 4, 2010 - 10:57:52 PM

Identifiers

  • HAL Id : inria-00072194, version 1

Collections

Citation

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

Share

Metrics

Record views

148

Files downloads

125