Document Open Access Logo

Lax Bialgebras and Up-To Techniques for Weak Bisimulations

Authors Filippo Bonchi, Daniela Petrisan, Damien Pous, Jurriaan Rot

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2015.240.pdf
  • Filesize: 0.49 MB
  • 14 pages

Document Identifiers

Author Details

Filippo Bonchi
Daniela Petrisan
Damien Pous
Jurriaan Rot

Cite AsGet BibTex

Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot. Lax Bialgebras and Up-To Techniques for Weak Bisimulations. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 240-253, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.CONCUR.2015.240

Abstract

Up-to techniques are useful tools for optimising proofs of behavioural equivalence of processes. Bisimulations up-to context can be safely used in any language specified by GSOS rules. We showed this result in a previous paper by exploiting the well-known observation by Turi and Plotkin that such languages form bialgebras. In this paper, we prove the soundness of up-to contextual closure for weak bisimulations of systems specified by cool rule formats, as defined by Bloom to ensure congruence of weak bisimilarity. However, the weak transition systems obtained from such cool rules give rise to lax bialgebras, rather than to bialgebras. Hence, to reach our goal, we extend our previously developed categorical framework to an ordered setting.
Keywords
  • Up-to techniques
  • weak bisimulation
  • (lax) bialgebras

Metrics

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

References

  1. L. Aceto, W. Fokkink, and C. Verhoef. Structural operational semantics. In Handbook of Process Algebra, pages 197-292. Elsevier, 2001. Google Scholar
  2. A. Balan and A. Kurz. Finitary functors: From Set to Preord and Poset. In CALCO, volume 6859 of LNCS, pages 85-99. Springer, 2011. Google Scholar
  3. A. Balan, A. Kurz, and J. Velebil. Positive fragments of coalgebraic logics. In CALCO, volume 8089 of LNCS, pages 51-65. Springer, 2013. Google Scholar
  4. B. Bloom. Structural operational semantics for weak bisimulations. Theor. Comput. Sci., 146(1&2):25-68, 1995. Google Scholar
  5. B. Bloom, S. Istrail, and A. R. Meyer. Bisimulation can't be traced. In POPL, pages 229-239. ACM, 1988. Google Scholar
  6. F. Bonchi, D. Petrişan, D. Pous, and J. Rot. Coinduction up-to in a fibrational setting. In CSL-LICS, page 20. ACM, 2014. Google Scholar
  7. F. Bonchi and D. Pous. Checking NFA equivalence with bisimulations up to congruence. In POPL, pages 457-468. ACM, 2013. Google Scholar
  8. D. Caucal. Graphes canoniques de graphes algébriques. ITA, 24:339-352, 1990. Google Scholar
  9. R. de Simone. Higher-level synchronising devices in Meije-SCCS. Theoretical Computer Science, 37(0):245-267, 1985. Google Scholar
  10. M. Fiore and S. Staton. Positive structural operational semantics and monotone distributive laws. In CMCS, page 8, 2010. Google Scholar
  11. C. Hermida and B. Jacobs. Structural induction and coinduction in a fibrational setting. Inf. and Comp., 145:107-152, 1997. Google Scholar
  12. J. Hughes and B. Jacobs. Simulations in coalgebra. TCS, 327(1-2):71-108, 2004. Google Scholar
  13. C.-K. Hur, G. Neis, D. Dreyer, and V. Vafeiadis. The power of parameterization in coinductive proof. In POPL'13, pages 193-206, New York, NY, USA, 2013. ACM. Google Scholar
  14. B. Jacobs. Introduction to coalgebra. Towards mathematics of states and observations, 2014. Draft. Google Scholar
  15. B. Klin. Bialgebras for structural operational semantics: An introduction. TCS, 412(38):5043-5069, 2011. Google Scholar
  16. R. Milner. Communication and Concurrency. Prentice Hall, 1989. Google Scholar
  17. U. Montanari and V. Sassone. CCS dynamic bisimulation is progressing. In MFCS, pages 346-356, 1991. Google Scholar
  18. D. Pous. Complete lattices and up-to techniques. In APLAS, volume 4807 of LNCS, pages 351-366. Springer, 2007. Google Scholar
  19. D. Pous and D. Sangiorgi. Enhancements of the bisimulation proof method. In Advanced Topics in Bisimulation and Coinduction, pages 233-289. Cambridge Univ. Press, 2012. Google Scholar
  20. D. Sangiorgi. Introduction to Bisimulation and Coinduction. Cambridge Univ. Press, 2011. Google Scholar
  21. A. M. Thijs. Simulation and fixpoint semantics. PhD thesis, Univ. of Groningen, 1996. Google Scholar
  22. D. Turi and G. D. Plotkin. Towards a mathematical operational semantics. In LICS, pages 280-291. IEEE, 1997. Google Scholar
  23. R. van Glabbeek. On cool congruence formats for weak bisimulations. Theoretical Computer Science, 412(28):3283-3302, 2011. Festschrift in Honour of Jan Bergstra. Google Scholar
  24. R. van Glabbeek and W. Weijland. Branching time and abstraction in bisimulation semantics. J. ACM, 43(3):555-600, 1996. Google Scholar
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact