Barbed bisimilarity is a widely-used behavioural equivalence for interactive systems: given a set of predicates (denoted “barbs” and representing basic observations on states) and a set of contexts (representing the possible execution environments), two systems are deemed to be equivalent if they verify the same barbs whenever inserted inside any of the chosen contexts. Despite its flexibility and expressiveness, this definition of equivalence is unsatisfactory, since often the quantification is over an infinite set of contexts, thus making barbed bisimilarity very hard to be verified. Should a labelled operational semantics be available, more efficient observational equivalences might be adopted. To this end, a series of techniques have been proposed to derive labelled transition systems (LTSs) from unlabeled ones, the main example being Leifer and Milner’s theory of reactive systems. The underlying intuition is that labels should be the “minimal” contexts that allow for a reduction step to be performed. However, minimality is difficult to asses, while the set of “intuitively” correct labels is often easily devised by the ingenuity of the researcher. This paper introduces a framework that characterises (weak) barbed bisimilarity via LTSs whose labels are (not necessarily minimal) contexts. Differently from previous proposals, our theory is not dependent on the way the labelled transitions are built, and it relies on a simple set-theoretical presentation for identifying those properties such an LTS should verify in order to (1) capture the barbed bisimilarities of the underlying system and (2) ensure that such bisimilarities are congruences. Furthermore, we adopt suitable proof techniques in order to make feasible the verification of such properties. To provide a test-bed for our formalism, we instantiate it by addressing the semantics of the Mobile Ambients calculus, recasting its (weak) barbed bisimilarities via label-based behavioural equivalences.
A general theory of barbs, contexts and labels
Bonchi F.;GADDUCCI, FABIO;MONREALE, GIACOMA
2014-01-01
Abstract
Barbed bisimilarity is a widely-used behavioural equivalence for interactive systems: given a set of predicates (denoted “barbs” and representing basic observations on states) and a set of contexts (representing the possible execution environments), two systems are deemed to be equivalent if they verify the same barbs whenever inserted inside any of the chosen contexts. Despite its flexibility and expressiveness, this definition of equivalence is unsatisfactory, since often the quantification is over an infinite set of contexts, thus making barbed bisimilarity very hard to be verified. Should a labelled operational semantics be available, more efficient observational equivalences might be adopted. To this end, a series of techniques have been proposed to derive labelled transition systems (LTSs) from unlabeled ones, the main example being Leifer and Milner’s theory of reactive systems. The underlying intuition is that labels should be the “minimal” contexts that allow for a reduction step to be performed. However, minimality is difficult to asses, while the set of “intuitively” correct labels is often easily devised by the ingenuity of the researcher. This paper introduces a framework that characterises (weak) barbed bisimilarity via LTSs whose labels are (not necessarily minimal) contexts. Differently from previous proposals, our theory is not dependent on the way the labelled transitions are built, and it relies on a simple set-theoretical presentation for identifying those properties such an LTS should verify in order to (1) capture the barbed bisimilarities of the underlying system and (2) ensure that such bisimilarities are congruences. Furthermore, we adopt suitable proof techniques in order to make feasible the verification of such properties. To provide a test-bed for our formalism, we instantiate it by addressing the semantics of the Mobile Ambients calculus, recasting its (weak) barbed bisimilarities via label-based behavioural equivalences.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
