关于基于状态与基于事件的系统之间对应关系的民间定理
计算机科学中的逻辑
2015-05-20 v1 形式语言与自动机理论
摘要
Kripke结构和标记迁移系统是并发理论中两种最突出的语义模型。这两种模型通常被认为具有等表达能力。人们可以找到许多将其中一种模型嵌入到另一种模型中的特设方法。我们基于De Nicola和Vaandrager的开创性工作，该工作牢固地建立了Kripke结构中的停顿等价与标记迁移系统中的发散敏感分支互模拟之间的对应关系。我们证明，他们的嵌入方法也可用于一系列其他感兴趣的等价关系，如强互模拟、模拟等价和迹等价。此外，我们扩展了De Nicola和Vaandrager的结果，表明存在额外的转换，允许在一个语义域中使用最小化技术，为这些等价关系在另一个语义域中获得最小代表。
引用
@article{arxiv.1011.0136,
title = {Folk Theorems on the Correspondence between State-Based and Event-Based Systems},
author = {M. A. Reniers and T. A. C. Willemse},
journal= {arXiv preprint arXiv:1011.0136},
year = {2015}
}
备注
Full version of SOFSEM 2011 paper