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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
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)
Abramsky, S.: The lazy lambda calculus. In: Turner, D.A. (ed.) Research topics in functional programming, pp. 65–116. Addison Wesley, Boston (1990)
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–26
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–175
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–365
Bartels, F.: Generalised coinduction. Math Struct Comput. Sci. 13(2), 321–348 (2003)
Bartels F (April 2004) On generalised coinduction and probabilistic specification formats. PhD thesis, CWI, Amsterdam
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)
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–164
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)
Boreale, M., De Nicola, R., Pugliese, R.: Basic observables for processes. Inf Comput 149(1), 77–98 (1999)
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)
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:17
Bezem, M., Klop, J.W., van Oostrom, V.: Diagram techniques for confluence. Inf Comput 141(2), 172–204 (1998)
Boreale, M.: Algebra, coalgebra, and minimization in polynomial differential equations. Log Methods Comput Sci 15(1), (2019)
Boudol G (1992) Asynchrony and the \(\pi \)-calculus. Technical Report RR-1702, INRIA-Sophia Antipolis
Bonchi F, Pous D (2013) Checking NFA equivalence with bisimulations up to congruence. In: Proceedings of the POPL, ACM, pp 457–468
Bonchi, F., Pous, D.: Hacking nondeterminism with induction and coinduction. Commun ACM 58(2), 87–95 (2015)
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:9
Basold H, Pous D, Rot J (2017) Monoidal company for accessible functors. In: Proceedings of the CALCO, volume 72 of LIPIcs. Schloss Dagstuhl
Blanchette JC, Popescu A, Traytel D (2015) Foundational extensible corecursion: a proof assistant perspective. In: ICFP, ACM, pp 192–204
Boreale M, Sangiorgi D (1998) Bisimulation in name-passing calculi without matching. In: LICS, IEEE, pp 165–175
Boreale, M., Sangiorgi, D.: Some congruence properties for pi-calculus bisimilarities. Theor Comput Sci 198(1–2), 159–176 (1998)
Caucal, D.: Graphes canoniques de graphes algébriques. ITA 24, 339–352 (1990)
Cardelli L, Gordon AD (1998) Mobile ambients. In: Nivat M (ed) Proceedings of the FoSSaCS '98, volume 1378 of LNCS. Springer, Berlin, pp 140–155
Christensen, S., Hüttel, H., Stirling, C.: Bisimulation equivalence is decidable for all context-free processes. Inf Comput 121(2), 143–148 (1995)
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:14
Danielsson NA (2018) Up-to techniques using sized types. PACMPL 2(POPL):43:1–43:28
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:16
Fournet, C., Gonthier, G.: A hierarchy of equivalences for asynchronous calculi. J Logic Algebr Program 63(1), 131–173 (2005)
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)
Gavazzo F (2019) Coinductive equivalences and metrics for higher-order languages with algebraic effects. PhD thesis, Univ. Bologna
Hirschkoff D (1999) Mise en oeuvre de preuves de bisimulation. PhD thesis, Ecole Nationale des Ponts et Chaussées
Hermida, C., Jacobs, B.: Structural induction and coinduction in a fibrational setting. Inf Comput 145(2), 107–152 (1998)
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)
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)
Hopcroft JE, Karp RM (1971) A linear algorithm for testing equivalence of finite automata. Technical Report 114, Cornell Univ., December
Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J ACM 32, 137–161 (1985)
Hur C-K, Neis G, Dreyer D, Vafeiadis V (2013) The power of parameterization in coinductive proof. In: POPL, ACM, pp 193–206
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–54
Jacobs, B.: Distributive laws for the coinductive solution of recursive equations. Inf Comput 204(4), 561–587 (2006)
Jacobs B (2016) Introduction to coalgebra: towards mathematics of states and observation, volume 59 of Cambridge tracts in theoretical computer science. Cambridge University Press, Cambridge
Jagadeesan, R., Pitcher, C., Riely, J.: Open bisimulation for aspects. Trans Asp Oriented Softw Dev 5, 72–132 (2009)
Klin, B.: Bialgebras for structural operational semantics: an introduction. Theor Comput Sci 412(38), 5043–5069 (2011)
Knaster, B.: Un théorème sur les fonctions d'ensembles. Annales de la Société Polonaise de Mathématiques 6, 133–134 (1928)
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–152
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)
Lassen SB (1998) Relational reasoning about functions and nondeterminism. PhD thesis, Department of Computer Science, University of Aarhus
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)
Lenisa, M.: From set-theoretic coinduction to coalgebraic coinduction: some results, some problems. Electr Notes Comput Sci 19, 2–22 (1999)
Dal Lago, U., Gavazzo, F.: Effectful normal form bisimulation. ESOP '19, volume 11423 of LNCS, pp. 263–292. Springer, Berin (2019)
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)
Milner R (1980) A calculus of communicating systems, volume 92 of LNCS. Springer, Berlin
Milner, R.: Calculi for synchrony and asynchrony. Theor Comput Sci 25, 269–310 (1983)
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, 1990
Milner, R.: Communication and concurrency. Prentice Hall, Englewood Cliffs (1989)
Milius, S., Moss, L.S., Schwencke, D.: Abstract GSOS rules and a modular treatment of recursive definitions. Log Methods Comput Sci 9(3), (2013)
Merro, M., Nardelli, F.Z.: Behavioural theory for mobile ambients. J ACM 52(6), 961–1023 (2005)
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)
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 Edinburgh
Newman, M.H.A.: On theories with a combinatorial definition of "equivalence". Ann Math 43(2), 223–243 (1942)
Niqui, M., Rutten, J.: A proof of Moessner's theorem by coinduction. Higher Order Symb Comput 24(3), 191–206 (2011)
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. Mayoh
Parrow J (1987) Notes `jp3' on label passing. Handwritten notes
Pitts AM (1995) An extension of Howe's construction to yield simulation-up-to-context results. Unpublished manuscript
Plotkin, G.D.: The origins of structural operational semantics. J Logic Algebr Program 60–61, 3–15 (2004)
Plotkin, G.D.: A structural approach to operational semantics. J Logic Algebr Program 60–61, 17–139 (2004)
Pous D (2005) Up-to techniques for weak bisimulation. In: Proceedings of the ICALP, volume 3580 of LNCS. Springer, Berlin, pp 730–741
Pous D (2006) Weak bisimulation up to elaboration. In: Proceedings of the CONCUR, volume 4137 of LNCS. Springer, Berlin, pp 390–405
Pous D (2007) Complete lattices and up-to techniques. In: Proceedings of the APLAS '07, volume 4807 of LNCS, pages 351–366. Springer, Belrin
Pous, D.: New up-to techniques for weak bisimulation. Theor Comput Sci 380(1–2), 164–180 (2007)
Pous, D.: Using bisimulation proof techniques for the analysis of distributed algorithms. Theor Comput Sci 402(2–3), 199–220 (2008)
Pous D (2016) Coinduction all the way up. In: Proceeding of the LICS, ACM, pp 307–316
Pous D, Rot J (2017) Companions, codensity, and causality. In: Proceedings of the FoSSaCS, volume 10203 of LNCS. Springer, Berlin, pp 106–123
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)
Pous D, Sangiorgi D Enhancements of the bisimulation proof method. In: Sangiorgi and Rutten [SR12]
Parrow, J., Weber, T.: The largest respectful function. Log Methods Comput Sci 12(2), (2016)
Rutten, J.: Universal coalgebra: a theory of systems. Theor Comput Sci 249(1), 3–80 (2000)
Rutten, J.: A coinductive calculus of streams. Math Struct Comput Sci 15(1), 93–147 (2005)
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 Edinburgh
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–83
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–479
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)
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)
Sangiorgi, D.: Asynchronous process calculi: the first- and higher-order paradigms. Theor Comput Sci 253(2), 311–350 (2001)
Sangiorgi, D.: On the origins of bisimulation and coinduction. ACM Trans Program Lang Syst 31(4), 15 (2009)
Sangiorgi, D.: Introduction to bisimulation and coinduction. Cambridge University Press, Cambridge (2012)
Sangiorgi D (2015) Equations, contractions, and unique solutions. In: Rajamani SK, Walker D (eds) POPL 2015, ACM, pp 421–432
Silva A, Bonchi F, Bonsangue M, Rutten J (2010) Generalizing the powerset construction, coalgebraically. In: FSTTCS, LIPIcs, pp 272–283. Schloss Dagstuhl
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 Society
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–46
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–172
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–74
Sangiorgi, D., Rutten, J. (eds.): Advanced topics in bisimulation and coinduction. Cambridge University Press, Cambridge (2012)
Staton, S.: Relating coalgebraic notions of bisimulation. Log Methods Comput Sci 7(1), (2011)
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–607
Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac J Math 5(2), 285–309 (1955)
Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. J ACM 22(2), 215–225 (1975)
Thomsen B (1989) A calculus of higher order communicating systems. In: POPL'89, ACM, pp 143–154
Turi D, Plotkin GD (1997) Towards a mathematical operational semantics. In: LICS, IEEE, pp 280–291
Uustalu, T., Vene, V., Pardo, A.: Recursion schemes from comonads. Nord J Comput 8(3), 366–390 (2001)
Walker DJ (1987) Bisimulation and divergence in CCS. Tech report, LFCS, Dept of Comp Sci, Edinburgh Univ
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).
Author information
Authors and Affiliations
Corresponding author
Additional information
Cliff Jones and Jose N. Oliveira
Publisher’s Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
About this article
Cite this article
Pous, D., Sangiorgi, D. Bisimulation and Coinduction Enhancements: A Historical Perspective. Form Asp Comp 31, 733–749 (2019). https://doi.org/10.1007/s00165-019-00497-w
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-019-00497-w