Abstract
Reactive systems, proposed by Leifer and Milner, represent a meta-framework aimed at deriving behavioral congruences for those specification formalisms whose operational semantics is provided by rewriting rules. Despite its applicability, reactive systems suffered so far from two main drawbacks. First of all, no technique was found for recovering a set of inference rules, e.g. in the so-called SOS style, for describing the distilled observational semantics. Most importantly, the efforts focused on strong bisimilarity, tackling neither weak nor barbed semantics.
Our paper addresses both issues, instantiating them on a calculus whose semantics is still in a flux: Cardelli and Gordon’s mobile ambients.
While the solution to the first issue is tailored over our case study, we provide a general framework for recasting (weak) barbed equivalence in the reactive systems formalism. Moreover, we prove that our proposal captures the behavioural semantics for mobile ambients proposed by Rathke and Sobociński and by Merro and Zappa Nardelli.
Partly supported by the EU FP6-IST IP 16004 SEnSOria and carried out during the first author’s tenure of an ERCIM “Alain Bensoussa” Fellowship Programme.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
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)
Bonchi, F., König, B., Montanari, U.: Saturated semantics for reactive systems. In: Logic in Computer Science, pp. 69–80. IEEE Computer Society, Los Alamitos (2006)
Bonchi, F.: Abstract Semantics by Observable Contexts. PhD thesis, Department of Informatics, University of Pisa (2008)
Milner, R.: Bigraphs for petri nets. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 686–701. Springer, Heidelberg (2004)
Sassone, V., Sobociński, P.: A congruence for Petri nets. In: Petri Nets and Graph Transformation. ENTCS, vol. 127, pp. 107–120. Elsevier, Amsterdam (2005)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Milner, R.: Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, Cambridge (1999)
Milner, R., Sangiorgi, D.: Barbed bisimulation. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 685–695. Springer, Heidelberg (1992)
Cardelli, L., Gordon, A.: Mobile ambients. TCS 240(1), 177–213 (2000)
Bonchi, F., Gadducci, F., Monreale, G.V.: Labelled transitions for mobile ambients (as synthesized via a graphical encoding). In: Expressiveness in Concurrency. ENTCS. Elsevier, Amsterdam (forthcoming, 2008)
Rathke, J., Sobociński, P.: Deriving structural labelled transitions for mobile ambients. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 462–476. Springer, Heidelberg (2008)
Merro, M., Zappa Nardelli, F.: Behavioral theory for mobile ambients. Journal of the ACM 52(6), 961–1023 (2005)
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)
Sassone, V., Sobociński, P.: Reactive systems over cospans. In: Logic in Computer Science, pp. 311–320. IEEE Computer Society, Los Alamitos (2005)
Plotkin, G.D.: A structural approach to operational semantics. Journal of Logic and Algebraic Programming 60-61, 17–139 (2004)
Milner, R.: Pure bigraphs: Structure and dynamics. Information and Computation 204(1), 60–122 (2006)
Bonchi, F., Gadducci, F., König, B.: Process bisimulation via a graphical encoding. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 168–183. Springer, Heidelberg (2006)
Milner, R.: Local bigraphs and confluence: Two conjectures. In: Expressiveness in Concurrency. ENTCS, vol. 175, pp. 65–73. Elsevier, Amsterdam (2007)
Di Gianantonio, P., Honsel, F., Lenisa, M.: RPO, second-order contexts, and λ-calculus. In: Amadio, R. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 334–349. Springer, Heidelberg (2008)
Jensen, O., Milner, R.: Bigraphs and transitions. In: Principles of Programming Languages, pp. 38–49. ACM Press, New York (2003)
Grohmann, D., Miculan, M.: Reactive systems over directed bigraphs. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 380–394. Springer, Heidelberg (2007)
Fournet, C., Gonthier, G.: A hierarchy of equivalences for asynchronous calculi. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 844–855. Springer, Heidelberg (1998)
Honda, K., Yoshida, N.: On reduction-based process semantics. TCS 151(2), 437–486 (1995)
Rathke, J., Sassone, V., Sobocinski, P.: Semantic barbs and biorthogonality. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 302–316. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bonchi, F., Gadducci, F., Monreale, G.V. (2009). Reactive Systems, Barbed Semantics, and the Mobile Ambients. In: de Alfaro, L. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2009. Lecture Notes in Computer Science, vol 5504. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00596-1_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-00596-1_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00595-4
Online ISBN: 978-3-642-00596-1
eBook Packages: Computer ScienceComputer Science (R0)