一句话：证明完全并发互模拟与 i-因果网互模拟在有限有界 Petri 网上可判定，推广了安全网结果。
本文研究真并发语义下等价关系在 Petri 网上的可判定性。作者证明了两个结果：经典的（强）完全并发互模拟（fully-concurrent bisimilarity，等价于保持历史互模拟）以及新提出的 i-因果网互模拟（i-causal-net bisimilarity，它比因果网互模拟稍粗）对于有限有界 Petri 网都是可判定的。证明方法推广了 Vogler 用于证明（强）完全并发互模拟在有限安全 Petri 网上可判定的有序标识（ordered marking）证明技术。该工作将可判定性从有限安全网扩展到更一般的有限有界网，并覆盖了新的因果网互模拟变体。
We prove that the well-known (strong) fully-concurrent bisimilarity and the novel i-causal-net bisimilarity, which is a sligtlhy coarser variant of causal-net bisimilarity, are decidable for finite bounded Petri nets. The proofs are based on a generalization of the ordered marking proof technique that Vogler used to demonstrate that (strong) fully-concurrent bisimilarity (or, equivalently, history-preserving bisimilarity) is decidable on finite safe nets.
@article{paperbot2157,
title = {Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets},
author = {Arnaldo Cesco and Roberto Gorrieri},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 4},
year = {2023},
doi = {10.46298/lmcs-19(4:37)2023}
}