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, 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 for our system, more efficient observational equivalences might be adopted. To this end, a series of techniques have been proposed to derive labelled transition systems (LTSs) from unlabelled ones, the main example being Leifer and Milner’s reactive systems. The underlying intuition is that labels are the “minimal” contexts that allow for a reduction to be performed.
We introduce a framework that characterizes (weak) barbed bisimilarity via transition systems whose labels are (possibly minimal) contexts. Differently from other proposals, our theory is not dependent on the way LTSs are built, and it relies on a simple set-theoretical presentation. To provide a test-bed for our formalism, we instantiate it by addressing the semantics of mobile ambients and HoCore, recasting the (weak) barbed bisimilarities of these calculi via label-based behavioural equivalences.
The first author has been supported by CNRS PEPS CoGIP. The second and third author have been partially supported by the EU FP7-ICT IP ASCEns and by the MIUR PRIN SisteR (PRIN 20088HXMYN).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Birkedal, L., Debois, S., Hildebrandt, T.T.: On the Construction of Sorted Reactive Systems. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 218–232. Springer, Heidelberg (2008)
Bonchi, F., Gadducci, F., Monreale, G.V.: Labelled transitions for mobile ambients (as synthesized via a graphical encoding). In: Hildebrandt, T., Gorla, D. (eds.) EXPRESS 2008. ENTCS, vol. 242(1), pp. 73–98. Elsevier, Amsterdam (2009)
Bonchi, F., Gadducci, F., Monreale, G.V.: On barbs and labels in reactive systems. In: Klin, B., Sobocinski, P. (eds.) SOS 2009. EPTCS, vol. 18, pp. 46–61 (2009)
Bonchi, F., Gadducci, F., Monreale, G.: Reactive Systems, Barbed Semantics, and the Mobile Ambients. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 272–287. Springer, Heidelberg (2009)
Bonchi, F., Montanari, U.: Symbolic semantics revisited. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 395–412. Springer, Heidelberg (2008)
Bonchi, F., Gadducci, F., König, B.: Synthesising CCS bisimulation using graph rewriting. Information and Computation 207(1), 14–40 (2009)
Cardelli, L., Gordon, A.: Mobile ambients. TCS 240(1), 177–213 (2000)
Ehrig, H., König, B.: Deriving bisimulation congruences in the DPO approach to graph rewriting with borrowed contexts. Mathematical Structures in Computer Science 16(6), 1133–1163 (2006)
Klin, B., Sassone, V., Sobociński, P.: Labels from Reductions: Towards a General Theory. In: Fiadeiro, J.L., Harman, N.A., Roggenbach, M., Rutten, J. (eds.) CALCO 2005. LNCS, vol. 3629, pp. 30–50. Springer, Heidelberg (2005)
Lanese, I., Pérez, J.A., Sangiorgi, D., Schmitt, A.: On the expressiveness and decidability of higher-order process calculi. Information and Computation 209(2), 198–226 (2011)
Leifer, J., Milner, R.: Deriving Bisimulation Congruences for Reactive Systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 243–258. Springer, Heidelberg (2000)
Merro, M., Zappa Nardelli, F.: Behavioral theory for mobile ambients. Journal of the ACM 52(6), 961–1023 (2005)
Milner, R., Sangiorgi, D.: Barbed Bisimulation. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 685–695. Springer, Heidelberg (1992)
Rathke, J., Sassone, V., Sobociński, P.: Semantic Barbs and Biorthogonality. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 302–316. Springer, Heidelberg (2007)
Rathke, J., Sobocinski, P.: Deconstructing behavioural theories of mobility. In: Ausiello, G., Karhumäki, J., Mauri, G., Ong, C.H.L. (eds.) IFP TCS 2008. IFIP, vol. 273, pp. 507–520. Springer, Heidelberg (2008)
Rathke, J., Sobocinski, P.: Deriving structural labelled transitions for mobile ambients. Information and Computation 208(10), 1221–1242 (2010)
Sassone, V., Sobociński, P.: Reactive systems over cospans. In: LICS 2005, pp. 311–320. IEEE Computer Society Press, Los Alamitos (2005)
Schmitt, A., Stefani, J.-B.: The Kell Calculus: A Family of Higher-Order Distributed Process Calcul. In: Priami, C., Quaglia, P. (eds.) GC 2004. LNCS, vol. 3267, pp. 146–178. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bonchi, F., Gadducci, F., Monreale, G.V. (2011). Towards a General Theory of Barbs, Contexts and Labels. In: Yang, H. (eds) Programming Languages and Systems. APLAS 2011. Lecture Notes in Computer Science, vol 7078. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25318-8_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-25318-8_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-25317-1
Online ISBN: 978-3-642-25318-8
eBook Packages: Computer ScienceComputer Science (R0)