Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 1 - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2002

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

Résumé

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.

Domaines

Autre [cs.OH]
Fichier principal
Vignette du fichier
RR-4394.pdf (558.93 Ko) Télécharger le fichier
Loading...

Dates et versions

inria-00072194 , version 1 (23-05-2006)

Identifiants

  • HAL Id : inria-00072194 , version 1

Citer

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

Partager

Gmail Facebook X LinkedIn More