论文标题

抽象的一致性标准较弱

Abstract Congruence Criteria for Weak Bisimilarity

论文作者

Tsampas, Stelios, Williams, Christian, Nuyts, Andreas, Devriese, Dominique, Piessens, Frank

论文摘要

我们在操作语义上介绍了三个一般的构图标准,并证明,当这三个共同满足时,它们会保证弱分配是一种一致性。我们的工作建立在Turi和Plotkin的数学操作语义以及Brengos弱分离的煤层方法上。我们以各种成功和失败的示例演示了每个标准,并与Bloom和Van Glabbeek的简单WB酷规则形式建立了正式的联系。此外,我们表明,这三个标准从Bonchi等人的意义上诱导了Lax模型。

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.

扫码加入交流群

加入微信交流群

微信交流群二维码

扫码加入学术交流群,获取更多资源