Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 - 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 2

Résumé

This paper is the second in a series of two. It relies on its companion, Part 1, to motivate the central problem addressed by the series, namely: how to synthesise labelled transitions for reactive systems and how to prove congruence results for operational equivalences and preorders defined above those transitions. The purpose of this paper is (i) to show that the hypotheses required of functorial reactive systems from Part 1, for example the sliding properties of IPO (idem pushout) squares, are indeed satisfied for functors of a general form; (ii) to illustrate an example of a functorial reactive system based on Milner's action calculi, which satisfy the RPO (relative pushout) hypothesis required in the proofs of congruence from Part 1.

Domaines

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

Dates et versions

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

Identifiants

  • HAL Id : inria-00072193 , version 1

Citer

James J. Leifer. Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2. [Research Report] RR-4395, INRIA. 2002. ⟨inria-00072193⟩
34 Consultations
41 Téléchargements

Partager

Gmail Facebook X LinkedIn More