开放Petri网的双相似性与行为保持重配置
计算机科学中的逻辑
2015-07-01 v2
摘要
我们提出了一个用于规范以Petri网建模的系统之行为保持重配置的框架。该框架基于开放网，这是对普通位置/变迁网的一种温和推广，适用于对可能与周围环境交互的开放系统进行建模，并配备了一种基于余极限的组合操作。我们证明了开放网上的自然双相似性概念相对于组合操作是同余关系。所考虑的行为等价性因观测的选择而异，观测可以是单次点火或并行步骤。此外，我们考虑了在存在不可观测动作时出现的这些等价性的弱形式。我们还提供了一种用于简化双相似性证明的up-to技术。该理论用于识别合适的重配置规则类（采用双推图重写方法），这些规则的应用保持了网的观测语义。
引用
@article{arxiv.0809.4115,
title = {Bisimilarity and Behaviour-Preserving Reconfigurations of Open Petri Nets},
author = {Paolo Baldan and Andrea Corradini and Hartmut Ehrig and Reiko Heckel and Barbara König},
journal= {arXiv preprint arXiv:0809.4115},
year = {2015}
}
备注
To appear in "Logical Methods in Computer Science", 41 pages