结构保持互模拟，支持CCSP的操作Petri网语义
计算机科学中的逻辑
2015-09-22 v1
摘要
1987年，Ernst-Rüdiger Olderog 为 CCSP（Milner 的 CCS 与 Hoare 的 CSP 的并）的一个子集提供了操作化 Petri 网语义。它为子集中的每个进程项分配一个带标签的安全库所/变迁网。为证明该方法的正确性，Olderog 确立了两点一致：(1) 与 CCSP 的标准交错语义在强互模拟等价下一致；(2) 与 CCSP 算子的标准指称解释在 Petri 网意义上，直至某种完全尊重网因果结构的合适语义等价下一致。对于后者，他采用了线性时间语义等价，即具有相同的因果网。本文加强了 (2)，采用了该语义的一种新的分支时间版本——结构保持互模拟——且此外保持必然性。我确立了它是 CCSP 算子的一个同余。
引用
@article{arxiv.1509.05842,
title = {Structure Preserving Bisimilarity, Supporting an Operational Petri Net Semantics of CCSP},
author = {Rob van Glabbeek},
journal= {arXiv preprint arXiv:1509.05842},
year = {2015}
}