Advertisement

Bisimulation and Coinduction Enhancements: A Historical Perspective

  • Damien Pous
  • Davide SangiorgiEmail author
Article
  • 12 Downloads

Abstract

Bisimulation is an instance of coinduction. Both bisimulation and coinduction are today widely used, in many areas of Computer Science, as well as outside Computer Science. Over, roughly, the last 25 years, enhancements of the principles and methods related to bisimulation and coinduction (i.e., techniques to make proofs shorter and simpler) have become a research topic on its own. In the paper the origins and the developments of the topic are reviewed.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Notes

Acknowledgements

We would like to thank the referees for many useful comments. Sangiorgi acknowledges support from the MIUPRIN project ‘Analysis of Program Analyses’ (ASPRA, ID 201784YSZ5_004) and the H2020-MSCA-RISE project ID 778233 “Behavioural Application Program Interfaces (BEHAPI)”. Pous was supported by the European Research Council (ERC) under the European Union’s Horizon 2020 programme (CoVeCe, grant agreement No 678157).

References

  1. [ABLP17]
    Aristizábal, A., Biernacki, D., Lenglet, S., Polesiuk, P.: Environmental bisimulations for delimited-control operators with dynamic prompt generation. Log Methods Comput Sci 13(3), (2017)Google Scholar
  2. [Abr90]
    Abramsky, S.: The lazy lambda calculus. In: Turner, D.A. (ed.) Research topics in functional programming, pp. 65–116. Addison Wesley, Boston (1990)Google Scholar
  3. [AG98]
    Abadi M, Gordon AD (1998) A bisimulation method for cryptographic protocols. In: Hankin C (ed) Proceedings of the ESOP'98, volume 1381 of LNCS. Springer, Berlin, pp 12–26CrossRefGoogle Scholar
  4. [AH91]
    Arun-Kumar S, Hennessy M (1991) An efficiency preorder for processes. In: Proceedings of the TACS '91, volume 526 of Lecture notes in computer science. Springer, Berlin, pp 152–175Google Scholar
  5. [AM89]
    Aczel P, Mendler NP (1989) A final coalgebra theorem. In: Proceedings of the category theory and computer science, volume 389 of LNCS. Springer, Belrin, pp 357–365Google Scholar
  6. [Bar03]
    Bartels, F.: Generalised coinduction. Math Struct Comput. Sci. 13(2), 321–348 (2003)CrossRefGoogle Scholar
  7. [Bar04]
    Bartels F (April 2004) On generalised coinduction and probabilistic specification formats. PhD thesis, CWI, AmsterdamGoogle Scholar
  8. [BBB+17]
    Biendarra, J., Blanchette, J.C., Bouzy, A., Desharnais, M., Fleury, M., Hölzl, J., Kuncar, O., Lochbihler, A., Meier, F., Panny, L., Popescu, A., Sternagel, C., Thiemann, R., Traytel, D.: Foundational (co)datatypes and (co)recursion for higher-order logic. FroCoS, volume 10483 of LNCS, pp. 3–21. Springer, Belrin (2017)Google Scholar
  9. [BBG98]
    Bravetti M, Bernardo M, Gorrieri R (1998) A note on the congruence proof for recursion in markovian bisimulation equivalence. In: Priami C (ed) Proceedings of the 6th internation workshop on process algebras and performance modeling (PAPM '98), pp 153–164Google Scholar
  10. [BBL+17]
    Blanchette, J.C., Bouzy, A., Lochbihler, A., Popescu, A., Traytel, D.: Friends with benefits–implementing corecursion in foundational proof assistants. ESOP, volume 10201 of LNCS, pp. 111–140. Springer, Berlin (2017)Google Scholar
  11. [BDP99]
    Boreale, M., De Nicola, R., Pugliese, R.: Basic observables for processes. Inf Comput 149(1), 77–98 (1999)MathSciNetzbMATHCrossRefGoogle Scholar
  12. [BKK17]
    Bonchi, F., König, B., Sebastian, Küpper: Up-to techniques for weighted systems. TACAS, volume 10205 of LNCS, pp. 535–552. Springer, Berlin (2017)Google Scholar
  13. [BKP18]
    Bonchi F, König B, Petrisan D (2018) Up-to techniques for behavioural metrics via fibrations. In: CONCUR, volume 118 of LIPIcs, Schloss Dagstuhl, pp 17:1–17:17Google Scholar
  14. [BKvO98]
    Bezem, M., Klop, J.W., van Oostrom, V.: Diagram techniques for confluence. Inf Comput 141(2), 172–204 (1998)MathSciNetzbMATHCrossRefGoogle Scholar
  15. [Bor19]
    Boreale, M.: Algebra, coalgebra, and minimization in polynomial differential equations. Log Methods Comput Sci 15(1), (2019)Google Scholar
  16. [Bou92]
    Boudol G (1992) Asynchrony and the \(\pi \)-calculus. Technical Report RR-1702, INRIA-Sophia AntipolisGoogle Scholar
  17. [BP13]
    Bonchi F, Pous D (2013) Checking NFA equivalence with bisimulations up to congruence. In: Proceedings of the POPL, ACM, pp 457–468zbMATHCrossRefGoogle Scholar
  18. [BP15]
    Bonchi, F., Pous, D.: Hacking nondeterminism with induction and coinduction. Commun ACM 58(2), 87–95 (2015)CrossRefGoogle Scholar
  19. [BPPR14]
    Bonchi F, PetriÅŸan D, Pous D, Rot J (2014) Coinduction up-to in a fibrational setting. In: Proceeding of the CSL-LICS, ACM, pp 20:1–20:9Google Scholar
  20. [BPR17]
    Basold H, Pous D, Rot J (2017) Monoidal company for accessible functors. In: Proceedings of the CALCO, volume 72 of LIPIcs. Schloss DagstuhlGoogle Scholar
  21. [BPT15]
    Blanchette JC, Popescu A, Traytel D (2015) Foundational extensible corecursion: a proof assistant perspective. In: ICFP, ACM, pp 192–204Google Scholar
  22. [BS98a]
    Boreale M, Sangiorgi D (1998) Bisimulation in name-passing calculi without matching. In: LICS, IEEE, pp 165–175Google Scholar
  23. [BS98b]
    Boreale, M., Sangiorgi, D.: Some congruence properties for pi-calculus bisimilarities. Theor Comput Sci 198(1–2), 159–176 (1998)zbMATHCrossRefGoogle Scholar
  24. [Cau90]
    Caucal, D.: Graphes canoniques de graphes algébriques. ITA 24, 339–352 (1990)MathSciNetGoogle Scholar
  25. [CG98]
    Cardelli L, Gordon AD (1998) Mobile ambients. In: Nivat M (ed) Proceedings of the FoSSaCS '98, volume 1378 of LNCS. Springer, Berlin, pp 140–155Google Scholar
  26. [CHS95]
    Christensen, S., Hüttel, H., Stirling, C.: Bisimulation equivalence is decidable for all context-free processes. Inf Comput 121(2), 143–148 (1995)MathSciNetzbMATHCrossRefGoogle Scholar
  27. [CPV16]
    Chatzikokolakis K, Palamidessi C, Vignudelli V (2016) Up-to techniques for generalized bisimulation metrics. In: Desharnais J, Jagadeesan R (eds) Proceedings of the CONCUR 2016, volume 59 of LIPIcs, Schloss Dagstuhl, pp 35:1–35:14Google Scholar
  28. [Dan18]
    Danielsson NA (2018) Up-to techniques using sized types. PACMPL 2(POPL):43:1–43:28CrossRefGoogle Scholar
  29. [DHS17]
    Durier A, Hirschkoff D, Sangiorgi D (2017) Divergence and unique solution of equations. In: Meyer R, Nestmann U (eds) 28th International conference on concurrency theory, CONCUR 2017, volume 85 of LIPIcs, Schloss Dagstuhl, pp 11:1–11:16Google Scholar
  30. [FG05]
    Fournet, C., Gonthier, G.: A hierarchy of equivalences for asynchronous calculi. J Logic Algebr Program 63(1), 131–173 (2005)MathSciNetzbMATHCrossRefGoogle Scholar
  31. [FM91]
    Fernandez, J.-C., Mounier, L.: "On the Fly" verification of behavioural equivalences and preorders. CAV, volume 575 of LNCS, pp. 181–191. Springer, Belin (1991)Google Scholar
  32. [Gav19]
    Gavazzo F (2019) Coinductive equivalences and metrics for higher-order languages with algebraic effects. PhD thesis, Univ. BolognaGoogle Scholar
  33. [Hir99]
    Hirschkoff D (1999) Mise en oeuvre de preuves de bisimulation. PhD thesis, Ecole Nationale des Ponts et ChausséesGoogle Scholar
  34. [HJ98]
    Hermida, C., Jacobs, B.: Structural induction and coinduction in a fibrational setting. Inf Comput 145(2), 107–152 (1998)MathSciNetzbMATHCrossRefGoogle Scholar
  35. [HJM96a]
    Hirshfeld, Y., Jerrum, M., Moller, F.: A polynomial algorithm for deciding bisimilarity of normed context-free processes. Theor Comput Sci 158(1&2), 143–159 (1996)MathSciNetzbMATHCrossRefGoogle Scholar
  36. [HJM96b]
    Hirshfeld, Y., Jerrum, M., Moller, F.: A polynomial-time algorithm for deciding bisimulation equivalence of normed basic parallel processes. Math Struct Comput Sci 6(3), 251–259 (1996)MathSciNetzbMATHCrossRefGoogle Scholar
  37. [HK71]
    Hopcroft JE, Karp RM (1971) A linear algorithm for testing equivalence of finite automata. Technical Report 114, Cornell Univ., DecemberGoogle Scholar
  38. [HM85]
    Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J ACM 32, 137–161 (1985)MathSciNetzbMATHCrossRefGoogle Scholar
  39. [HNDV13]
    Hur C-K, Neis G, Dreyer D, Vafeiadis V (2013) The power of parameterization in coinductive proof. In: POPL, ACM, pp 193–206Google Scholar
  40. [HT91]
    Honda K, Tokoro M (1991) A small calculus for concurrent objects. In: Proceedings of the workshop on object-based concurrent programming, OOPSLA/ECOOP '90, ACM, New York, NY, USA, pp 50–54Google Scholar
  41. [Jac06]
    Jacobs, B.: Distributive laws for the coinductive solution of recursive equations. Inf Comput 204(4), 561–587 (2006)MathSciNetzbMATHCrossRefGoogle Scholar
  42. [Jac16]
    Jacobs B (2016) Introduction to coalgebra: towards mathematics of states and observation, volume 59 of Cambridge tracts in theoretical computer science. Cambridge University Press, CambridgeGoogle Scholar
  43. [JPR09]
    Jagadeesan, R., Pitcher, C., Riely, J.: Open bisimulation for aspects. Trans Asp Oriented Softw Dev 5, 72–132 (2009)zbMATHCrossRefGoogle Scholar
  44. [Kli11]
    Klin, B.: Bialgebras for structural operational semantics: an introduction. Theor Comput Sci 412(38), 5043–5069 (2011)MathSciNetzbMATHCrossRefGoogle Scholar
  45. [Kna28]
    Knaster, B.: Un théorème sur les fonctions d'ensembles. Annales de la Société Polonaise de Mathématiques 6, 133–134 (1928)zbMATHGoogle Scholar
  46. [KW06]
    Koutavas V, Wand M (2006) Small bisimulations for reasoning about higher-order imperative programs. In: Proceedings of the 33rd ACM SIGPLAN-SIGACT symposium on principles of programming languages, pp 141–152Google Scholar
  47. [Las98a]
    Lassen, S.B.: Relational reasoning about contexts. In: Gordon, A.D., Pitts, A.M. (eds.) Higher order operational techniques in semantics. Cambridge University Press, Cambridge (1998)Google Scholar
  48. [Las98b]
    Lassen SB (1998) Relational reasoning about functions and nondeterminism. PhD thesis, Department of Computer Science, University of AarhusGoogle Scholar
  49. [Las99]
    Lassen, S.B.: Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context. Electr Notes Theor Comput Sci 20, 346–374 (1999)MathSciNetzbMATHCrossRefGoogle Scholar
  50. [Len99]
    Lenisa, M.: From set-theoretic coinduction to coalgebraic coinduction: some results, some problems. Electr Notes Comput Sci 19, 2–22 (1999)MathSciNetzbMATHCrossRefGoogle Scholar
  51. [LG19]
    Dal Lago, U., Gavazzo, F.: Effectful normal form bisimulation. ESOP '19, volume 11423 of LNCS, pp. 263–292. Springer, Berin (2019)Google Scholar
  52. [LPW00]
    Lenisa, M., Power, J., Watanabe, H.: Distributivity for endofunctors, pointed and co-pointed endofunctors, monads and comonads. Electr Notes Comput Sci 33, 230–260 (2000)MathSciNetzbMATHCrossRefGoogle Scholar
  53. [Mil80]
    Milner R (1980) A calculus of communicating systems, volume 92 of LNCS. Springer, BerlinGoogle Scholar
  54. [Mil83]
    Milner, R.: Calculi for synchrony and asynchrony. Theor Comput Sci 25, 269–310 (1983)MathSciNetzbMATHCrossRefGoogle Scholar
  55. [Mil87]
    Milner R (1987) Operational and algebraic semantics of concurrent processes. Notes, November 1987. Appeared as Tech Rep ECS-LFCS-88-46, Edinburgh 1988, and later as a chapter in Handbook of Theoretical Computer Science (vol. B), pp 1201–1242, MIT Press, 1990Google Scholar
  56. [Mil89]
    Milner, R.: Communication and concurrency. Prentice Hall, Englewood Cliffs (1989)zbMATHGoogle Scholar
  57. [MMS13]
    Milius, S., Moss, L.S., Schwencke, D.: Abstract GSOS rules and a modular treatment of recursive definitions. Log Methods Comput Sci 9(3), (2013)Google Scholar
  58. [MN05]
    Merro, M., Nardelli, F.Z.: Behavioural theory for mobile ambients. J ACM 52(6), 961–1023 (2005)MathSciNetzbMATHCrossRefGoogle Scholar
  59. [MPW89]
    Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, Part I and II. Technical report ECS-LFCS-89-85 and -86, University of Edinburgh, 1989. Appeared in J. Inf. Comp. 100, 1–77 (1992)CrossRefGoogle Scholar
  60. [MT91]
    Milner R, Tofte M (1988) Co-induction in relational semantics. Theor Comput Sci 87:209–220, 1991. Also Tech. Rep. ECS-LFCS-88-65, University of EdinburghMathSciNetzbMATHCrossRefGoogle Scholar
  61. [New42]
    Newman, M.H.A.: On theories with a combinatorial definition of "equivalence". Ann Math 43(2), 223–243 (1942)MathSciNetzbMATHCrossRefGoogle Scholar
  62. [NR11]
    Niqui, M., Rutten, J.: A proof of Moessner's theorem by coinduction. Higher Order Symb Comput 24(3), 191–206 (2011)MathSciNetzbMATHCrossRefGoogle Scholar
  63. [Par81]
    Park D (1981) A new equivalence notion for communicating systems. In: Maurer G (ed) Bulletin EATCS, volume 14, pages 78–80, 1981. Abstract of the talk presented at the SecondWorkshop on the Semantics of Programming Languages, BadHonnef, March 16–20 1981. Abstracts collected in the Bulletin by B. MayohGoogle Scholar
  64. [Par87]
    Parrow J (1987) Notes `jp3' on label passing. Handwritten notesGoogle Scholar
  65. [Pit95]
    Pitts AM (1995) An extension of Howe's construction to yield simulation-up-to-context results. Unpublished manuscriptGoogle Scholar
  66. [Plo04a]
    Plotkin, G.D.: The origins of structural operational semantics. J Logic Algebr Program 60–61, 3–15 (2004)MathSciNetzbMATHCrossRefGoogle Scholar
  67. [Plo04b]
    Plotkin, G.D.: A structural approach to operational semantics. J Logic Algebr Program 60–61, 17–139 (2004)MathSciNetzbMATHGoogle Scholar
  68. [Pou05]
    Pous D (2005) Up-to techniques for weak bisimulation. In: Proceedings of the ICALP, volume 3580 of LNCS. Springer, Berlin, pp 730–741CrossRefGoogle Scholar
  69. [Pou06]
    Pous D (2006) Weak bisimulation up to elaboration. In: Proceedings of the CONCUR, volume 4137 of LNCS. Springer, Berlin, pp 390–405CrossRefGoogle Scholar
  70. [Pou07a]
    Pous D (2007) Complete lattices and up-to techniques. In: Proceedings of the APLAS '07, volume 4807 of LNCS, pages 351–366. Springer, BelrinzbMATHCrossRefGoogle Scholar
  71. [Pou07b]
    Pous, D.: New up-to techniques for weak bisimulation. Theor Comput Sci 380(1–2), 164–180 (2007)MathSciNetzbMATHCrossRefGoogle Scholar
  72. [Pou08]
    Pous, D.: Using bisimulation proof techniques for the analysis of distributed algorithms. Theor Comput Sci 402(2–3), 199–220 (2008)zbMATHCrossRefGoogle Scholar
  73. [Pou16]
    Pous D (2016) Coinduction all the way up. In: Proceeding of the LICS, ACM, pp 307–316Google Scholar
  74. [PR17]
    Pous D, Rot J (2017) Companions, codensity, and causality. In: Proceedings of the FoSSaCS, volume 10203 of LNCS. Springer, Berlin, pp 106–123Google Scholar
  75. [PS97]
    Pierce B, Sangiorgi D (2000) Behavioral equivalence in the polymorphic pi-calculus. In: Proceedings of the 24th POPL. ACM Press, 1997. Full paper in JACM 47(3)Google Scholar
  76. [PS12]
    Pous D, Sangiorgi D Enhancements of the bisimulation proof method. In: Sangiorgi and Rutten [SR12]Google Scholar
  77. [PW16]
    Parrow, J., Weber, T.: The largest respectful function. Log Methods Comput Sci 12(2), (2016)Google Scholar
  78. [Rut00]
    Rutten, J.: Universal coalgebra: a theory of systems. Theor Comput Sci 249(1), 3–80 (2000)MathSciNetzbMATHCrossRefGoogle Scholar
  79. [Rut05]
    Rutten, J.: A coinductive calculus of streams. Math Struct Comput Sci 15(1), 93–147 (2005)MathSciNetzbMATHCrossRefGoogle Scholar
  80. [San92]
    Sangiorgi D (1992) Expressing mobility in process algebras: first-order and higher-order paradigms. PhD thesis CST–99–93, Department of Computer Science, University of EdinburghGoogle Scholar
  81. [San94]
    Sangiorgi D (1996) Locality and true-concurrency in calculi for mobile processes. In: TACS'94, volume 789 of LNCS, pages 405–424. Springer Verlag, 1994. Full version in TCS, vol 155, 39–83Google Scholar
  82. [San95]
    Sangiorgi D (1998) On the bisimulation proof method. In: Wiedermann J, Háiek P (eds) Proceedings of the MFCS'95, volume 969 of LNCS, pp 479–488. Springer, Berlin 1995. Full version in J. MSCS, vol 8, pp 447–479MathSciNetzbMATHCrossRefGoogle Scholar
  83. [San98]
    Sands, D.: Improvement theory and its applications. In: Gordon, A.D., Pitts, A.M. (eds.) Higher order operational techniques in semantics, publications of the Newton Institute, pp. 275–306. Cambridge University Press (1998)Google Scholar
  84. [San00]
    Sangiorgi, D.: Lazy functions and mobile processes. In: Plotkin, G., Stirling, C., Tofte, M. (eds.) Proof, language and interaction: essays in honour of Robin Milner. MIT Press, Cambridge (2000)Google Scholar
  85. [San01]
    Sangiorgi, D.: Asynchronous process calculi: the first- and higher-order paradigms. Theor Comput Sci 253(2), 311–350 (2001)MathSciNetzbMATHCrossRefGoogle Scholar
  86. [San09]
    Sangiorgi, D.: On the origins of bisimulation and coinduction. ACM Trans Program Lang Syst 31(4), 15 (2009)CrossRefGoogle Scholar
  87. [San12]
    Sangiorgi, D.: Introduction to bisimulation and coinduction. Cambridge University Press, Cambridge (2012)zbMATHGoogle Scholar
  88. [San15]
    Sangiorgi D (2015) Equations, contractions, and unique solutions. In: Rajamani SK, Walker D (eds) POPL 2015, ACM, pp 421–432MathSciNetzbMATHCrossRefGoogle Scholar
  89. [SBBR10]
    Silva A, Bonchi F, Bonsangue M, Rutten J (2010) Generalizing the powerset construction, coalgebraically. In: FSTTCS, LIPIcs, pp 272–283. Schloss DagstuhlGoogle Scholar
  90. [SKS07]
    Sangiorgi D, Kobayashi N, Sumii E (2007) Environmental bisimulations for higher-order languages. In: Proceedings of the 22nd IEEE symposium on logic in computer science (LICS 2007), pp 293–302. IEEE Computer SocietyGoogle Scholar
  91. [SM92]
    Sangiorgi D, Milner R (1992) The problem of ``weak bisimulation up to''. In: Proceedings of the 3rd CONCUR, volume 630 of LNCS. Springer, Berlin, pp 32–46Google Scholar
  92. [SP04]
    Sumii E, Pierce BC (2004) A bisimulation for dynamic sealing. In: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on principles of programming languages, pp 161–172Google Scholar
  93. [SP05]
    Sumii E, Pierce BC (2005) A bisimulation for type abstraction and recursion. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on principles of programming languages, pp 63–74Google Scholar
  94. [SR12]
    Sangiorgi, D., Rutten, J. (eds.): Advanced topics in bisimulation and coinduction. Cambridge University Press, Cambridge (2012)zbMATHGoogle Scholar
  95. [Sta11]
    Staton, S.: Relating coalgebraic notions of bisimulation. Log Methods Comput Sci 7(1), (2011)Google Scholar
  96. [SV16]
    Sangiorgi D, Vignudelli V (2016) Environmental bisimulations for probabilistic higher-order languages. In: Bodík R, Majumdar R (eds) Proceedings of the POPL 2016, ACM, pp 595–607Google Scholar
  97. [Tar55]
    Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac J Math 5(2), 285–309 (1955)MathSciNetzbMATHCrossRefGoogle Scholar
  98. [Tar75]
    Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. J ACM 22(2), 215–225 (1975)MathSciNetzbMATHCrossRefGoogle Scholar
  99. [Tho89]
    Thomsen B (1989) A calculus of higher order communicating systems. In: POPL'89, ACM, pp 143–154Google Scholar
  100. [TP97]
    Turi D, Plotkin GD (1997) Towards a mathematical operational semantics. In: LICS, IEEE, pp 280–291Google Scholar
  101. [UVP01]
    Uustalu, T., Vene, V., Pardo, A.: Recursion schemes from comonads. Nord J Comput 8(3), 366–390 (2001)MathSciNetzbMATHGoogle Scholar
  102. [Wal87]
    Walker DJ (1987) Bisimulation and divergence in CCS. Tech report, LFCS, Dept of Comp Sci, Edinburgh UnivGoogle Scholar

Copyright information

© British Computer Society 2019

Authors and Affiliations

  1. 1.Univ Lyon, CNRS, EnsL, UCBL, LIPLyon Cedex 07France
  2. 2.University of BolognaBolognaItaly
  3. 3.INRIARocquencourtFrance

Personalised recommendations