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.

翻译：位置互模拟 $\sim_p$ 是有限Petri网的一种行为等价关系，最初在 \cite{ABS91} 中提出。与迄今为止提出的所有其他行为关系不同，它不是定义在有限网的标识上，而是定义在网的库所上，而库所的数量是有限的。\cite{ABS91} 声称位置互模拟 $\sim_p$ 是可判定的，但并未真正证明其可判定性。我们证明，可以用一个简单的算法判定 $\sim_p$，该算法本质上扫描所有库所关系（其数量有限）以检查它们是否为位置互模拟。我们还表明，$\sim_p$ 确实尊重Petri网预期的因果语义，因为它比因果网互模拟 \cite{Gor22} 更精细。此外，我们提出了一个稍粗的变体，称为d-位置互模拟 $\sim_d$，我们推测它是有限Petri网上可判定的最粗等价关系，完全尊重因果关系和分支时间（因为它比全并发互模拟 \cite{BDKP91} 更精细）。最后，讨论了另外两个更粗的变体，即i-位置互模拟和i-d-位置互模拟，它们仍然是可判定的，保留了Petri网的并发行为，但不尊重因果关系。这些结果为通过等价检验对有限Petri网建模的分布式系统进行形式验证开辟了道路。