Divergence and Unique Solution of Equations

Authors Adrien Durier, Daniel Hirschkoff, Davide Sangiorgi

Thumbnail PDF


  • Filesize: 479 kB
  • 16 pages

Document Identifiers

Author Details

Adrien Durier
Daniel Hirschkoff
Davide Sangiorgi

Cite AsGet BibTex

Adrien Durier, Daniel Hirschkoff, and Davide Sangiorgi. Divergence and Unique Solution of Equations. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


We study proof techniques for bisimilarity based on unique solution of equations. We draw inspiration from a result by Roscoe in the denotational setting of CSP and for failure semantics, essentially stating that an equation (or a system of equations) whose infinite unfolding never produces a divergence has the unique-solution property. We transport this result onto the operational setting of CCS and for bisimilarity. We then exploit the operational approach to: refine the theorem, distinguishing between different forms of divergence; derive an abstract formulation of the theorems, on generic LTSs; adapt the theorems to other equivalences such as trace equivalence, and to preorders such as trace inclusion. We compare the resulting techniques to enhancements of the bisimulation proof method (the ‘up-to techniques’). Finally, we study the theorems in name-passing calculi such as the asynchronous pi-calculus, and revisit the completeness proof of Milner’s encoding of the lambda-calculus into the pi-calculus for Lévy-Longo Trees.
  • Bisimilarity
  • unique solution of equations
  • termination
  • process calculi


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Luca Aceto, Wan Fokkink, and Chris Verhoef. Handbook of Process Algebra (J.A. Bergstra and A. Ponse and S.A. Smolka, editors), chapter Structural operational semantics. Elsevier Science, 2001. Google Scholar
  2. Jos C.M. Baeten, Twan Basten, and Michel A. Reniers. Process Algebra: Equational Theories of Communicating Processes. Cambridge University Press, 2010. Google Scholar
  3. Bard Bloom, Sorin Istrail, and Albert R. Meyer. Bisimulation can't be traced. In Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, pages 229-239, 1988. Google Scholar
  4. Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot. A general account of coinduction up-to. Acta Inf., 54(2):127-190, 2017. Google Scholar
  5. Stephen D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A theory of communicating sequential processes. J. ACM, 31(3):560-599, 1984. Google Scholar
  6. Stephen D. Brookes and A. W. Roscoe. An improved failures model for communicating processes. In Seminar on Concurrency, Carnegie-Mellon University, Pittsburg, PA, USA, pages 281-305, 1984. Google Scholar
  7. Romain Demangeon, Daniel Hirschkoff, and Davide Sangiorgi. Termination in impure concurrent languages. In CONCUR 2010 - Concurrency Theory, 21th International Conference, pages 328-342, 2010. Google Scholar
  8. Adrien Durier. Divergence and unique solution of equations in an abstract setting, Coq formal proof, 2017. URL: http://perso.ens-lyon.fr/adrien.durier/uniquesolution/.
  9. Wan Fokkink and Rob J. van Glabbeek. Divide and congruence II: delay and weak bisimilarity. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pages 778-787. ACM, 2016. Google Scholar
  10. Jan Friso Groote and Mohammad Reza Mousavi. Modeling and Analysis of Communicating Systems. MIT Press, 2014. Google Scholar
  11. Jan Friso Groote and Frits W. Vaandrager. Structured operational semantics and bisimulation as a congruence. Inf. Comput., 100(2):202-260, 1992. Google Scholar
  12. C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985. Google Scholar
  13. Robin Milner. Communication and concurrency. PHI Series in computer science. Prentice Hall, 1989. Google Scholar
  14. Robin Milner. Functions as processes. Mathematical Structures in Computer Science, 2(2):119-141, 1992. Google Scholar
  15. Robin Milner. Communicating and mobile systems - the Pi-calculus. Cambridge University Press, 1999. Google Scholar
  16. Mohammad Reza Mousavi, Michel A. Reniers, and Jan Friso Groote. SOS formats and meta-theory: 20 years after. Theor. Comput. Sci., 373(3):238-272, 2007. Google Scholar
  17. Damien Pous. Up to techniques for bisimulations. PhD thesis, ENS Lyon, February 2008. Google Scholar
  18. Damien Pous. Coinduction all the way up. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pages 307-316, 2016. Google Scholar
  19. Damien Pous and Davide Sangiorgi. Advanced Topics in Bisimulation and Coinduction (D. Sangiorgi and J. Rutten editors), chapter Enhancements of the coinductive proof method. Cambridge University Press, 2011. Google Scholar
  20. A. W. Roscoe. An alternative order for the failures model. J. Log. Comput., 2(5):557-577, 1992. Google Scholar
  21. A. W. Roscoe. The Theory and Practice of Concurrency. Prentice Hall PTR, Upper Saddle River, NJ, USA, 1997. Google Scholar
  22. A. W. Roscoe. Understanding Concurrent Systems. Springer, 2010. Google Scholar
  23. Jurriaan Rot, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Coalgebraic bisimulation-up-to. In SOFSEM 2013: Theory and Practice of Computer Science, 39th International Conference on Current Trends in Theory and Practice of Computer Science, pages 369-381, 2013. Google Scholar
  24. Davide Sangiorgi. Lazy functions and mobile processes. In G. Plotkin, C. Stirling, and M. Tofte, editors, Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, 2000. Google Scholar
  25. Davide Sangiorgi. Equations, contractions, and unique solutions. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, pages 421-432, 2015. Google Scholar
  26. Davide Sangiorgi and David Walker. The Pi-Calculus - a theory of mobile processes. Cambridge University Press, 2001. Google Scholar
  27. Davide Sangiorgi and Xian Xu. Trees from functions as processes. In 25th International Conference, CONCUR 2014, Rome, Italy, LNCS, pages 78-92. Springer Verlag, 2014. Google Scholar
  28. Rob J. van Glabbeek. The linear time-branching time spectrum (extended abstract). In CONCUR '90, Theories of Concurrency: Unification and Extension, Amsterdam, The Netherlands, August 27-30, 1990, Proceedings, pages 278-297, 1990. Google Scholar
  29. Rob J. van Glabbeek. On cool congruence formats for weak bisimulations. In Theoretical Aspects of Computing - ICTAC 2005, Second International Colloquium, pages 318-333, 2005. Google Scholar
  30. Nobuko Yoshida, Martin Berger, and Kohei Honda. Strong Normalisation in the Pi-Calculus. Information and Computation, 191(2):145-202, 2004. Google Scholar