Document Open Access Logo

Abstract Congruence Criteria for Weak Bisimilarity

Authors Stelios Tsampas , Christian Williams , Andreas Nuyts , Dominique Devriese , Frank Piessens



PDF
Thumbnail PDF

File

LIPIcs.MFCS.2021.88.pdf
  • Filesize: 0.91 MB
  • 23 pages

Document Identifiers

Author Details

Stelios Tsampas
  • KU Leuven, Belgium
Christian Williams
  • University of California, Riverside, CA, USA
Andreas Nuyts
  • Vrije Universiteit Brussel, Belgium
Dominique Devriese
  • Vrije Universiteit Brussel, Belgium
Frank Piessens
  • KU Leuven, Belgium

Acknowledgements

This research was partially funded by the Research Fund KU Leuven. Andreas Nuyts was supported by a grant of the Research Foundation – Flanders (FWO).

Cite AsGet BibTex

Stelios Tsampas, Christian Williams, Andreas Nuyts, Dominique Devriese, and Frank Piessens. Abstract Congruence Criteria for Weak Bisimilarity. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 88:1-88:23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.MFCS.2021.88

Abstract

We introduce three general compositionality criteria over operational semantics and prove that, when all three are satisfied together, they guarantee weak bisimulation being a congruence. Our work is founded upon Turi and Plotkin’s mathematical operational semantics and the coalgebraic approach to weak bisimulation by Brengos. We demonstrate each criterion with various examples of success and failure and establish a formal connection with the simply WB cool rule format of Bloom and van Glabbeek. In addition, we show that the three criteria induce lax models in the sense of Bonchi et al.

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
Keywords
  • Structural Operational Semantics
  • distributive laws
  • weak bisimilarity

Metrics

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

References

  1. Peter Aczel and Nax Paul Mendler. A final coalgebra theorem. In David H. Pitt, David E. Rydeheard, Peter Dybjer, Andrew M. Pitts, and Axel Poigné, editors, Category Theory and Computer Science, Manchester, UK, September 5-8, 1989, Proceedings, volume 389 of Lecture Notes in Computer Science, pages 357-365. Springer, 1989. URL: https://doi.org/10.1007/BFb0018361.
  2. Jirí Adámek, Paul Blain Levy, Stefan Milius, Lawrence S. Moss, and Lurdes Sousa. On final coalgebras of power-set functors and saturated trees - to george janelidze on the occasion of his sixtieth birthday. Applied Categorical Structures, 23(4):609-641, 2015. URL: https://doi.org/10.1007/s10485-014-9372-9.
  3. Christel Baier and Holger Hermanns. Weak bisimulation for fully probabilistic processes. In Orna Grumberg, editor, Computer Aided Verification, 9th International Conference, CAV '97, Haifa, Israel, June 22-25, 1997, Proceedings, volume 1254 of Lecture Notes in Computer Science, pages 119-130. Springer, 1997. URL: https://doi.org/10.1007/3-540-63166-6_14.
  4. Bard Bloom. Structural operational semantics for weak bisimulations. Theor. Comput. Sci., 146(1&2):25-68, 1995. URL: https://doi.org/10.1016/0304-3975(94)00152-9.
  5. Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot. Coinduction up-to in a fibrational setting. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14-18, 2014, pages 20:1-20:9. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603149.
  6. Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot. Lax bialgebras and up-to techniques for weak bisimulations. In Luca Aceto and David de Frutos-Escrig, editors, 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015, volume 42 of LIPIcs, pages 240-253. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2015.240.
  7. Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot. A general account of coinduction up-to. Acta Inf., 54(2):127-190, 2017. URL: https://doi.org/10.1007/s00236-016-0271-4.
  8. Tomasz Brengos. Weak bisimulation for coalgebras over order enriched monads. Logical Methods in Computer Science, 11(2), 2015. URL: https://doi.org/10.2168/LMCS-11(2:14)2015.
  9. Tomasz Brengos, Marino Miculan, and Marco Peressotti. Behavioural equivalences for coalgebras with unobservable moves. J. Log. Algebraic Methods Program., 84(6):826-852, 2015. URL: https://doi.org/10.1016/j.jlamp.2015.09.002.
  10. Derek Dreyer, Amal Ahmed, and Lars Birkedal. Logical step-indexed logical relations. Logical Methods in Computer Science, 7(2), 2011. URL: https://doi.org/10.2168/LMCS-7(2:16)2011.
  11. Marcelo Fiore and Sam Staton. Positive structural operational semantics and monotone distributive laws. In CMCS'10 Short Contributions, 2010. Google Scholar
  12. Sergey Goncharov and Dirk Pattinson. Coalgebraic weak bisimulation from recursive equations over monads. In Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias Koutsoupias, editors, Automata, Languages, and Programming - 41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part II, volume 8573 of Lecture Notes in Computer Science, pages 196-207. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-43951-7_17.
  13. Andrew D. Gordon. Bisimilarity as a theory of functional programming. Theor. Comput. Sci., 228(1-2):5-47, 1999. URL: https://doi.org/10.1016/S0304-3975(98)00353-3.
  14. Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic trace semantics via coinduction. Logical Methods in Computer Science, 3(4), 2007. URL: https://doi.org/10.2168/LMCS-3(4:11)2007.
  15. Douglas J. Howe. Equality in lazy computation systems. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), Pacific Grove, California, USA, June 5-8, 1989, pages 198-203. IEEE Computer Society, 1989. URL: https://doi.org/10.1109/LICS.1989.39174.
  16. Douglas J. Howe. Proving congruence of bisimulation in functional programming languages. Inf. Comput., 124(2):103-112, 1996. URL: https://doi.org/10.1006/inco.1996.0008.
  17. Bartek Klin. Bialgebras for structural operational semantics: An introduction. Theor. Comput. Sci., 412(38):5043-5069, 2011. URL: https://doi.org/10.1016/j.tcs.2011.03.023.
  18. Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer, 1980. URL: https://doi.org/10.1007/3-540-10235-3.
  19. Robin Milner. Communication and concurrency. PHI Series in computer science. Prentice Hall, 1989. Google Scholar
  20. James H. Morris. Lambda-Calculus Models of Programming Languages. PhD thesis, Massachusetts Institute of Technology, 1968. Google Scholar
  21. C.-H. L. Ong. Correspondence between Operational and Denotational Semantics: The Full Abstraction Problem for PCF, page 269?356. Oxford University Press, Inc., USA, 1995. Google Scholar
  22. Andrew M. Pitts. Reasoning about local variables with operationally-based logical relations. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996, pages 152-163. IEEE Computer Society, 1996. URL: https://doi.org/10.1109/LICS.1996.561314.
  23. Andrew M. Pitts. A note on logical relations between semantics and syntax. Log. J. IGPL, 5(4):589-601, 1997. URL: https://doi.org/10.1093/jigpal/5.4.589.
  24. Andrew M. Pitts. Parametric polymorphism and operational equivalence. Math. Struct. Comput. Sci., 10(3):321-359, 2000. URL: http://journals.cambridge.org/action/displayAbstract?aid=44651.
  25. Andrew M. Pitts. Typed operational reasoning. In Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 7. The MIT Press, 2004. Google Scholar
  26. Gordon D. Plotkin. A structural approach to operational semantics. J. Log. Algebr. Program., 60-61:17-139, 2004. Google Scholar
  27. Andrei Popescu. Weak bisimilarity coalgebraically. In Algebra and Coalgebra in Computer Science, Third International Conference, CALCO 2009, Udine, Italy, September 7-10, 2009. Proceedings, pages 157-172, 2009. URL: https://doi.org/10.1007/978-3-642-03741-2_12.
  28. Damien Pous and Davide Sangiorgi. Enhancements of the bisimulation proof method. In Davide Sangiorgi and Jan J. M. M. Rutten, editors, Advanced Topics in Bisimulation and Coinduction, volume 52 of Cambridge tracts in theoretical computer science, pages 233-289. Cambridge University Press, 2012. Google Scholar
  29. Jan Rothe and Dragan Masulovic. Towards weak bisimulation for coalgebras. Electr. Notes Theor. Comput. Sci., 68(1):32-46, 2002. URL: https://doi.org/10.1016/S1571-0661(04)80499-7.
  30. Jan J. M. M. Rutten. A note on coinduction and weak bisimilarity for while programs. ITA, 33(4/5):393-400, 1999. URL: https://doi.org/10.1051/ita:1999125.
  31. Davide Sangiorgi and Robin Milner. The problem of "weak bisimulation up to". In Rance Cleaveland, editor, CONCUR '92, Third International Conference on Concurrency Theory, Stony Brook, NY, USA, August 24-27, 1992, Proceedings, volume 630 of Lecture Notes in Computer Science, pages 32-46. Springer, 1992. URL: https://doi.org/10.1007/BFb0084781.
  32. Sam Staton. Relating coalgebraic notions of bisimulation. Log. Methods Comput. Sci., 7(1), 2011. URL: https://doi.org/10.2168/LMCS-7(1:13)2011.
  33. Stelios Tsampas, Andreas Nuyts, Dominique Devriese, and Frank Piessens. A categorical approach to secure compilation. In Daniela Petrisan and Jurriaan Rot, editors, Coalgebraic Methods in Computer Science - 15th IFIP WG 1.3 International Workshop, CMCS 2020, Colocated with ETAPS 2020, Dublin, Ireland, April 25-26, 2020, Proceedings, volume 12094 of Lecture Notes in Computer Science, pages 155-179. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-57201-3_9.
  34. Daniele Turi. Categorical modelling of structural operational rules: Case studies. In Category Theory and Computer Science, 7th International Conference, CTCS '97, Santa Margherita Ligure, Italy, September 4-6, 1997, Proceedings, pages 127-146, 1997. URL: https://doi.org/10.1007/BFb0026985.
  35. Daniele Turi and Gordon D. Plotkin. Towards a mathematical operational semantics. In Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997, pages 280-291, 1997. URL: https://doi.org/10.1109/LICS.1997.614955.
  36. Rob J. van Glabbeek. Full abstraction in structural operational semantics (extended abstract). In Maurice Nivat, Charles Rattray, Teodor Rus, and Giuseppe Scollo, editors, Algebraic Methodology and Software Technology (AMAST '93), Proceedings of the Third International Conference on Methodology and Software Technology, University of Twente, Enschede, The Netherlands, 21-25 June, 1993, Workshops in Computing, pages 75-82. Springer, 1993. Google Scholar
  37. Rob J. van Glabbeek. On cool congruence formats for weak bisimulations. Theor. Comput. Sci., 412(28):3283-3302, 2011. URL: https://doi.org/10.1016/j.tcs.2011.02.036.
  38. Mitchell Wand. Fixed-point constructions in order-enriched categories. Theor. Comput. Sci., 8:13-30, 1979. URL: https://doi.org/10.1016/0304-3975(79)90053-7.
  39. Glynn Winskel and Mogens Nielsen. Models for concurrency. DAIMI Report Series, 22(463), November 1993. URL: https://doi.org/10.7146/dpb.v22i463.6936.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail