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
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