LIPIcs.CONCUR.2015.240.pdf
- Filesize: 0.49 MB
- 14 pages
Document
Lax Bialgebras and Up-To Techniques for Weak Bisimulations
Authors
-
Part of:
Volume:
26th International Conference on Concurrency Theory (CONCUR 2015)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Concurrency Theory (CONCUR) - License:
Creative Commons Attribution 3.0 Unported license
- Publication date: 2015-08-26
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
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)
0PDF Downloads