Abstract
Up-to techniques have been introduced to enhance the bisimulation proof method for establishing bisimilarity results. While up-to techniques for strong bisimilarity are well understood, in the weak case they come as a collection of unrelated results, and lack a unified presentation. We propose a uniform and modular theory of up-to techniques for weak bisimulation that captures existing proof technology and introduces new techniques. Some proofs rely on non trivial – and new – commutation results based on termination guarantees.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
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
Arun-Kumar, S., Hennessy, M.: An efficiency preorder for processes. Acta Informatica 29(9), 737–760 (1992)
Bezem, M., Klop, J.W., van Oostrom, V.: Diagram techniques for confluence. Information and Computation 141(2), 172–204 (1998)
Fournet, C.: The Join-Calculus: a Calculus for Distributed Mobile Programming. PhD thesis, Ecole Polytechnique (1998)
Hirschkoff, D., Pous, D., Sangiorgi, D.: An Efficient Abstract Machine for Safe Ambients. Technical Report 2004–63, LIP – ENS Lyon, 2004. An extended abstract appeared in the proceedings of COORDINATION 2005 (2005)
Pous, D.: Up-to Techniques for Weak Bisimulation. Technical Report 2005–16, LIP – ENS Lyon (2005)
Pous, D.: Web appendix of this paper (2005), Available at http://perso.ens-lyon.fr/damien.pous/upto
INRIA projet Logical. The Coq proof assistant, http://coq.inria.fr/
Sangiorgi, D.: On the Bisimulation Proof Method. Mathematical Structures in Computer Science 8, 447–479 (1998)
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)
TeReSe. Term Rewriting Systems, Cambridge University Press, Cambridge (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pous, D. (2005). Up-to Techniques for Weak Bisimulation. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds) Automata, Languages and Programming. ICALP 2005. Lecture Notes in Computer Science, vol 3580. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11523468_59
Download citation
DOI: https://doi.org/10.1007/11523468_59
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27580-0
Online ISBN: 978-3-540-31691-6
eBook Packages: Computer ScienceComputer Science (R0)