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]
Loading...