Lax Bialgebras and Up-To Techniques for Weak Bisimulations
| Autor: | Bonchi, F., Petrisan, D.L., Pous, D., Rot, J.C., Aceto, L. |
|---|---|
| Přispěvatelé: | Aceto, L., Laboratoire de l'Informatique du Parallélisme (LIP), Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-École normale supérieure - Lyon (ENS Lyon), Preuves et Langages (PLUME), Université de Lyon-École normale supérieure - Lyon (ENS Lyon)-Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), Radboud university [Nijmegen], Leiden Institute of Advanced Computer Science [Leiden] (LIACS), Universiteit Leiden [Leiden], ANR-12-IS02-0001,PACE,Processus non-standard: Analyse, Coinduction, Expressivité(2012), ANR-10-LABX-0070,MILYON,Community of mathematics and fundamental computer science in Lyon(2010), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Radboud University [Nijmegen], Universiteit Leiden, École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL) |
| Rok vydání: | 2015 |
| Předmět: |
(Lax) bialgebras
Up- to techniques Weak bisimulation Software 000 Computer science knowledge general works Data Science [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 0102 computer and information sciences 02 engineering and technology Leibniz International Proceedings in Informatics 01 natural sciences 010201 computation theory & mathematics Computer Science::Logic in Computer Science Computer Science 0202 electrical engineering electronic engineering information engineering ComputingMethodologies_DOCUMENTANDTEXTPROCESSING 020201 artificial intelligence & image processing |
| Zdroj: | Aceto, L. (ed.), CONCUR 2015 : 26th International Conference on Concurrency Theory, 240-253. Dagstuhl : Schloss Dagstuhl STARTPAGE=240;ENDPAGE=253;ISSN=1868-8969;TITLE=Aceto, L. (ed.), CONCUR 2015 : 26th International Conference on Concurrency Theory Aceto, L. (ed.), CONCUR 2015 : 26th International Conference on Concurrency Theory, pp. 240-253 26th International Conference on Concurrency Theory (CONCUR) 26th International Conference on Concurrency Theory (CONCUR), Sep 2015, Madrid, Spain. ⟨10.4230/LIPIcs.CONCUR.2015.240⟩ |
| ISSN: | 1868-8969 |
| DOI: | 10.4230/LIPIcs.CONCUR.2015.240⟩ |
| Popis: | International audience; 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. Weshowed this result in a previous paper by exploiting the well-known observation by Turi andPlotkin that such languages form bialgebras. In this paper, we prove the soundness of up-tocontextual closure for weak bisimulations of systems specified by cool rule formats, as defined byBloom to ensure congruence of weak bisimilarity. However, the weak transition systems obtainedfrom such cool rules give rise to lax bialgebras, rather than to bialgebras. Hence, to reach ourgoal, we extend our previously developed categorical framework to an ordered setting. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|