有限有界Petri网两种真并发等价关系的可判定性
计算机科学中的逻辑
2024-02-14 v9
摘要
我们证明了著名的（强）全并发互模拟以及新颖的i-因果网互模拟（它是因果网互模拟的一种略粗的变体）对于有限有界Petri网是可判定的。证明基于Vogler用于证明（强）全并发互模拟（或等价地，保历史互模拟）在有限安全网上可判定的有序标记证明技术的推广。
引用
@article{arxiv.2104.14856,
title = {Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets},
author = {Arnaldo Cesco and Roberto Gorrieri},
journal= {arXiv preprint arXiv:2104.14856},
year = {2024}
}