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

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

Cited literature [2 references]  Display  Hide  Download

https://hal.inria.fr/inria-00072193
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 8:02:39 PM
Last modification on : Friday, May 25, 2018 - 12:02:03 PM
Long-term archiving on : Sunday, April 4, 2010 - 10:57:50 PM

Identifiers

  • HAL Id : inria-00072193, version 1

Collections

Citation

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

Share

Metrics

Record views

89

Files downloads

126