Hostname: page-component-6bf8c574d5-vmclg Total loading time: 0 Render date: 2025-02-22T17:27:30.262Z Has data issue: false hasContentIssue false
  • English
  • Français

Enhanced coalgebraic bisimulation

Published online by Cambridge University Press:  09 December 2015

JURRIAAN ROT ,
FILIPPO BONCHI ,
MARCELLO BONSANGUE ,
DAMIEN POUS ,
JAN RUTTEN  and
ALEXANDRA SILVA
JURRIAAN ROT
Affiliation:
Université de Lyon, CNRS, ENS de Lyon, UCBL, LIP, 46 Allée d'Italie, 69364 Lyon, France Email: jurriaan.rot@ens-lyon.fr
FILIPPO BONCHI
Affiliation:
CNRS, Plume team, LIP (UMR 5668, ENS de Lyon, UCBL, Université de Lyon), 46 Allée d'Italie, 69364 Lyon, France
MARCELLO BONSANGUE
Affiliation:
LIACS - Leiden University, Niels Bohrweg 1, 2333CA, The Netherlands Email: m.m.bonsangue@liacs.leidenuniv.nl Centrum Wiskunde en Informatica (CWI), Science Park 123, 1098 XG Amsterdam, The Netherlands
DAMIEN POUS
Affiliation:
CNRS, Plume team, LIP (UMR 5668, ENS de Lyon, UCBL, Université de Lyon), 46 Allée d'Italie, 69364 Lyon, France
JAN RUTTEN
Affiliation:
Centrum Wiskunde en Informatica (CWI), Science Park 123, 1098 XG Amsterdam, The Netherlands Radboud University Nijmegen, Toernooiveld 212, 6525 EC Nijmegen, The Netherlands
ALEXANDRA SILVA
Affiliation:
University College London, Gower Street, London WC1E 6BT, U.K.
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

We present a systematic study of bisimulation-up-to techniques for coalgebras. This enhances the bisimulation proof method for a large class of state based systems, including labelled transition systems but also stream systems and weighted automata. Our approach allows for compositional reasoning about the soundness of enhancements. Applications include the soundness of bisimulation up to bisimilarity, up to equivalence and up to congruence. All in all, this gives a powerful and modular framework for simplified coinductive proofs of equivalence.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 27 , Special Issue 7: Special Issue: Coalgebraic Logic , October 2017 , pp. 1236 - 1264
Copyright
Copyright © Cambridge University Press 2015 

References

Aceto, L., Fokkink, W. and Verhoef, C. (2001). Structural operational semantics. In: Handbook of Process Algebra, Elsevier Science, 197–292.Google Scholar
Aczel, P. and Mendler, N. (1989). A final coalgebra theorem. In: Category Theory and Computer Science, LNCS, volume 389, Springer, 357–365.Google Scholar
Adámek, J., Koubek, V. and Velebil, J. (2000). A duality between infinitary varieties and algebraic theories. Commentationes Mathematicae Universitatis Carolinae 41 (3) 529–542.Google Scholar
Bartels, F. (2004). On Generalised Coinduction and Probabilistic Specification Formats. Ph.D. thesis, CWI, Amsterdam.Google Scholar
Berstel, J. and Reutenauer, C. (1988). Rational Series and Their Languages, Springer.Google Scholar
Bloom, B., Istrail, S. and Meyer, A. (1995). Bisimulation can't be traced. Journal of ACM 42 (1) 232–268.Google Scholar
Bonchi, F., Bonsangue, M., Boreale, M., Rutten, J. and Silva, A. (2012). A coalgebraic perspective on linear weighted automata. Information and Computation 211 77–105.Google Scholar
Bonchi, F., Petrisan, D., Pous, D. and Rot, J. (2014). Coinduction up-to in a fibrational setting. In: Henzinger, T.A. and Miller, D. (eds.) CSL-LICS 2014, ACM, 20.Google Scholar
Bonchi, F. and Pous, D. (2013). Checking NFA equivalence with bisimulations up to congruence. In: Giacobazzi, R. and Cousot, R. (eds.) POPL, ACM, 457–468.Google Scholar
Bonsangue, M.M., Hansen, H.H., Kurz, A. and Rot, J. (2013). Presenting distributive laws. In: Heckel, R. and Milius, S. (eds.) CALCO. Lecture Notes in Computer Science 8089, Springer, Berlin, 95–109.Google Scholar
Buchholz, P. and Kemper, P. (2001). Quantifying the dynamic behavior of process algebras. In: de Alfaro, L. and Gilmore, S. (eds.) PAPM-PROBMIV. Lecture Notes in Computer Science, Springer, Berlin, 184–199.Google Scholar
Conway, J. (1971). Regular Algebra and Finite Machines, Chapman and Hall.Google Scholar
Endrullis, J., Hendriks, D. and Bodin, M. (2013). Circular coinduction in Coq using bisimulation-up-to techniques. In: Blazy, S., Paulin-Mohring, C. and Pichardie, D. (eds.) ITP 2013. LNCS 7998, Springer, Berlin, 354–369.Google Scholar
Gorín, D. and Schröder, L. (2013). Simulations and bisimulations for coalgebraic modal logics. In: Heckel, R. and Milius, S. (eds.) Proceedings of the 5th International Conference on Algebra and Coalgebra in Computer Science (CALCO 2013). Lecture Notes in Computer Science 8089, Springer, Berlin, 253–266.Google Scholar
Gumm, H. (1999). Elements of the general theory of coalgebras. In: LUATCS 99, Rand Afrikaans University, South Africa.Google Scholar
Gumm, H. and Schröder, T. (2000). Coalgebraic structure from weak limit preserving functors. Electronic Notes in Theoretical Computer Science 33 111–131.Google Scholar
Gumm, H.P. and Schröder, T. (2001). Monoid-labeled transition systems. Electronic Notes in Theoretical Computer Science 44 (1) 185–204.Google Scholar
Hermida, C. and Jacobs, B. (1998). Structural induction and coinduction in a fibrational setting. Information and Computation 145 (2) 107–152.Google Scholar
Hopcroft, J. and Karp, R. (1971). A linear algorithm for testing equivalence of finite automata. Technical Report 114, Cornell Univ.Google Scholar
Klin, B. (2009). Structural operational semantics for weighted transition systems. In: Palsberg, J. (eds.) Semantics and Algebraic Specification. Lecture Notes in Computer Science 5700, Springer, Berlin, 121–139.Google Scholar
Klin, B. (2011). Bialgebras for structural operational semantics: An introduction. TCS 412 (38) 5043–5069.Google Scholar
Lenisa, M. (1999). From set-theoretic coinduction to coalgebraic coinduction: Some results, some problems. ENTCS 19 2–22.Google Scholar
Lenisa, M., Power, J. and Watanabe, H. (2000). Distributivity for endofunctors, pointed and co-pointed endofunctors, monads and comonads. ENTCS 33 230–260.Google Scholar
Levy, P.B. (2011). Similarity quotients as final coalgebras. In: Hofmann, M. (eds.) FOSSACS 2011. Lecture Notes in Computer Science 6604, Springer, Berlin, 27–41.CrossRefGoogle Scholar
Luo, L. (2006). An effective coalgebraic bisimulation proof method. Electronic Notes in Theoretical Computer Science 164 (1) 105–119.Google Scholar
Marti, J. and Venema, Y. (2012). Lax extensions of coalgebra functors. In: Pattinson, D. and Schröder, L. (eds.) 11th International Workshop on Coalgebraic Methods in Computer Science (CMCS 2012). Lecture Notes in Computer Science, Springer, Berlin, 7399 150–169.Google Scholar
Milner, R. (1980). A Calculus of Communicating Systems, Lecture Notes in Computer Science, volume 92, Springer.CrossRefGoogle Scholar
Milner, R. (1983). Calculi for synchrony and asynchrony. TCS 25 (3) 267–310.Google Scholar
Park, D. (1981). Concurrency and automata on infinite sequences. In: Deussen, P. (eds.) Theoretical Computer Science. Lecture Notes in Computer Science 104, Springer, Berlin, 167–183.Google Scholar
Pous, D. (2007). Complete lattices and up-to techniques. In: Proceedings of the APLAS. Springer Lecture Notes in Computer Science 4807 351–366.CrossRefGoogle Scholar
Pous, D. and Sangiorgi, D. (2012). Enhancements of the bisimulation proof method. In: Advanced Topics in Bisimulation and Coinduction, Cambridge University Press, 233–289.Google Scholar
Rot, J., Bonsangue, M. and Rutten, J. (2013a). Coalgebraic bisimulation-up-to. In: van Emde Boas, P., Groen, F., Italiano, G., Nawrocki, J. and Sack, H. (eds.) SOFSEM. Springer Lecture Notes in Computer Science 7741 369–381.Google Scholar
Rot, J., Bonsangue, M. and Rutten, J. (2013b). Coinductive proof techniques for language equivalence. In: Dediu, A.-H., Martín-Vide, C. and Truthe, B. (eds.) LATA. Lecture Notes in Computer Science 7810, Springer, Berlin, 480–492 Google Scholar
Rutten, J. (1998). Relators and metric bisimulations. ENTCS 11 252–258.Google Scholar
Rutten, J. (2000). Universal coalgebra: A theory of systems. TCS 249 (1) 3–80.Google Scholar
Rutten, J. (2003). Behavioural differential equations: A coinductive calculus of streams, automata, and power series. TCS 308 (1–3) 1–53.CrossRefGoogle Scholar
Salomaa, A. and Soittola, M. (1978). Automata-Theoretic Aspects of Formal Power Series, Texts and Monographs on Computer Science, Springer.Google Scholar
Sangiorgi, D. (1998). On the bisimulation proof method. Mathematical Structures in Computer Science 8 (5) 447–479.Google Scholar
Sangiorgi, D. (2012). An introduction to Bisimulation and Coinduction, Cambridge University Press.Google Scholar
Staton, S. (2011). Relating coalgebraic notions of bisimulation. LMCS 7 (1).Google Scholar
Trnková, V. (1980). General theory of relational automata. Fundamenta Informaticae 3 (2) 189–234.Google Scholar
Turi, D. and Plotkin, G. (1997). Towards a mathematical operational semantics. In: LICS, IEEE Computer Society, 280–291.Google Scholar
Winter, J., Bonsangue, M.M. and Rutten, J.J.M.M. (2011). Context-free languages, coalgebraically. In: Corradini, A., Klin, B. and Cîrstea, C. (eds.) CALCO. Lecture Notes in Computer Science 6859, Springer, Berlin, 359–376.Google Scholar
Zhou, X., Li, Y., Li, W., Qiao, H. and Shu, Z. (2010). Bisimulation proof methods in a path-based specification language for polynomial coalgebras. In: APLAS. Lecture Notes in Computer Science 6461, Springer, Berlin, 239–254.Google Scholar