License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2015.240
URN: urn:nbn:de:0030-drops-53709
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5370/
Bonchi, Filippo ;
Petrisan, Daniela ;
Pous, Damien ;
Rot, Jurriaan
Lax Bialgebras and Up-To Techniques for Weak Bisimulations
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.
BibTeX - Entry
@InProceedings{bonchi_et_al:LIPIcs:2015:5370,
author = {Filippo Bonchi and Daniela Petrisan and Damien Pous and Jurriaan Rot},
title = {{Lax Bialgebras and Up-To Techniques for Weak Bisimulations}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {240--253},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-91-0},
ISSN = {1868-8969},
year = {2015},
volume = {42},
editor = {Luca Aceto and David de Frutos Escrig},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5370},
URN = {urn:nbn:de:0030-drops-53709},
doi = {10.4230/LIPIcs.CONCUR.2015.240},
annote = {Keywords: Up-to techniques, weak bisimulation, (lax) bialgebras}
}
Keywords: |
|
Up-to techniques, weak bisimulation, (lax) bialgebras |
Collection: |
|
26th International Conference on Concurrency Theory (CONCUR 2015) |
Issue Date: |
|
2015 |
Date of publication: |
|
26.08.2015 |