Place Bisimilarity is Decidable, Indeed!（位置互模拟确实可判定！）
Place Bisimilarity is Decidable, Indeed!
AI总结：
本文证明了有限 Petri 网上的位置互模拟可判定性，提出简单扫描算法，并引入更粗的 d-位置变体，为分布式系统形式化验证铺路。
摘要：
位置互模拟 $\sim_p$ 是有限 Petri 网的一种行为等价关系，最初在 \cite{ABS91} 中提出。与迄今提出的所有其他行为关系不同，它不是定义在有限网的标记上，而是定义在其位置（place）上，而位置的数量是有限的。位置互模拟 $\sim_p$ 在 \cite{ABS91} 中被声称是可判定的，但其可判定性并未真正得到证明。我们表明，可以用一个简单的算法来判定 $\sim_p$，该算法本质上扫描所有位置关系（数量有限），以检查它们是否为位置互模拟。我们还表明，$\sim_p$ 确实尊重 Petri 网预期的因果语义，因为它比因果网互模拟 \cite{Gor22} 更精细。此外，我们提出一个稍微更粗的变体，称为 d-位置互模拟 $\sim_d$，我们猜想它是完全尊重因果关系和分支时间的最粗等价关系（因为它比全并发互模拟 \cite{BDKP91} 更精细），并且在有限 Petri 网上是可判定的。最后，讨论了两种更粗的变体，即 i-位置互模拟和 i-d-位置互模拟，它们仍然是可判定的，确实保留了 Petri 网的并发行为，但不尊重因果关系。这些结果为通过等价性检查对由有限 Petri 网建模的分布式系统进行形式化验证开辟了道路。
英文摘要：
Place bisimilarity $\sim_p$ is a behavioral equivalence for finite Petri nets, originally proposed in \cite{ABS91}, that, differently from all the other behavioral relations proposed so far, is not defined over the markings of a finite net, rather over its places, which are finitely many. Place bisimilarity $\sim_p$ was claimed decidable in \cite{ABS91}, but its decidability was not really proved. We show that it is possible to decide $\sim_p$ with a simple algorithm, which essentially scans all the place relations (which are finitely many) to check whether they are place bisimulations. We also show that $\sim_p$ does respect the intended causal semantics of Petri nets, as it is finer than causal-net bisimilarity \cite{Gor22}. Moreover, we propose a slightly coarser variant, we call d-place bisimilarity $\sim_d$, that we conjecture to be the coarsest equivalence, fully respecting causality and branching time (as it is finer than fully-concurrent bisimilarity \cite{BDKP91}), to be decidable on finite Petri nets. Finally, two even coarser variants are discussed, namely i-place and i-d-place bisimilarities, which are still decidable, do preserve the concurrent behavior of Petri nets, but do not respect causality. These results open the way towards formal verification (by equivalence checking) of distributed systems modeled by finite Petri nets.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
