Abstract
We illustrate the use of recent, non-trivial proof techniques for weak bisimulation by analysing a generic framework for the definition of distributed abstract machines based on a message-passing implementation. The definition of the framework comes from previous works on a specific abstract machine; however, its new presentation, as a parametrised process algebra, makes it suitable for a wider range of calculi.
A first version of the framework can be analysed using the standard bisimulation up to expansion proof technique. We show that in a second, optimised version, rather complex behaviours appear, for which more sophisticated techniques, relying on termination arguments, are necessary to establish behavioural equivalence.
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
Bidinger, P., Stefani, J.-B.: The Kell Calculus: Operational Semantics and Type System. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 109–123. Springer, Heidelberg (2003)
Cardelli, L., Gordon, A.: Mobile Ambients. In: Nivat, M. (ed.) ETAPS 1998 and FOSSACS 1998. LNCS, vol. 1378, pp. 140–155. Springer, Heidelberg (1998)
Castagna, G., Nardelli, F.Z.: The Seal Calculus Revisited. In: Agrawal, M., Seth, A.K. (eds.) FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science. LNCS, vol. 2556, pp. 85–96. Springer, Heidelberg (2002)
Fournet, C., Le Fessant, F., Maranget, L., Schmitt, A.: JoCaml: A Language for Concurrent Distributed and Mobile Programming. In: Jeuring, J., Jones, S.L.P. (eds.) AFP 2002. LNCS, vol. 2638, pp. 129–158. Springer, Heidelberg (2003)
Hirschkoff, D., Pous, D., Sangiorgi, D.: In: Jacquet, J.-M., Picco, G.P. (eds.) COORDINATION 2005. LNCS, vol. 3454, Springer, Heidelberg (2005)
Levi, F., Sangiorgi, D.: Mobile Safe Ambients. In: ACM Trans. on Progr. Lang. and Sys. vol. 25(1), pp. 1–69. ACM Press, New York (2003)
De Nicola, R., Ferrari, G.L., Pugliese, R.: KLAIM: A Kernel Language for Agents Interaction and Mobility. IEEE Trans. Software Eng. 24(5), 315–330 (1998)
Pous, D.: Up-to Techniques for Weak Bisimulation. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 730–741. Springer, Heidelberg (2005)
Sangiorgi, D., Milner, R.: The problem of Weak Bisimulation up to. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 32–46. Springer, Heidelberg (1992)
Sangiorgi, D., Valente, A.: A Distributed Abstract Machine for Safe Ambients. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, Springer, Heidelberg (2001)
Unyapoth, A., Sewell, P.: Nomadic pict: Correct Communication Infrastructure for Mobile Computation. In: Proc. 28th POPL, pp. 116–127. ACM Press, New York (2001)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pous, D. (2007). On Bisimulation Proofs for the Analysis of Distributed Abstract Machines. In: Montanari, U., Sannella, D., Bruni, R. (eds) Trustworthy Global Computing. TGC 2006. Lecture Notes in Computer Science, vol 4661. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75336-0_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-75336-0_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75333-9
Online ISBN: 978-3-540-75336-0
eBook Packages: Computer ScienceComputer Science (R0)