Abstract Congruence Criteria for Weak Bisimilarity
Logic in Computer Science
2021-10-14 v3 Category Theory
Abstract
We introduce three general compositionality criteria over operational semantics and prove that, when all three are satisfied together, they guarantee weak bisimulation being a congruence. Our work is founded upon Turi and Plotkin's mathematical operational semantics and the coalgebraic approach to weak bisimulation by Brengos. We demonstrate each criterion with various examples of success and failure and establish a formal connection with the simply WB cool rule format of Bloom and van Glabbeek. In addition, we show that the three criteria induce lax models in the sense of Bonchi et al.
Keywords
Cite
@article{arxiv.2010.07899,
title = {Abstract Congruence Criteria for Weak Bisimilarity},
author = {Stelios Tsampas and Christian Williams and Andreas Nuyts and Dominique Devriese and Frank Piessens},
journal= {arXiv preprint arXiv:2010.07899},
year = {2021}
}