Place bisimilarity is a behavioral equivalence for finite Petri nets, proposed in \cite{ABS91} and proved decidable in \cite{Gor21}. In this paper we propose an extension to finite Petri nets with silent moves of the place bisimulation idea, yielding {\em branching} place bisimilarity $\approx_p$, following the intuition of branching bisimilarity \cite{vGW96} on labeled transition systems. We also propose a slightly coarser variant, called branching {\em d-place} bisimilarity $\approx_d$, following the intuition of d-place bisimilarity in \cite{Gor21}. We prove that $\approx_p$ and $\approx_d$ are decidable equivalence relations. Moreover, we prove that $\approx_d$ is strictly finer than branching fully-concurrent bisimilarity \cite{Pin93,Gor20c}, essentially because $\approx_d$ does not consider as unobservable those $\tau$-labeled net transitions with pre-set size larger than one, i.e., those resulting from (multi-party) interaction.
翻译:位置互模拟性是有限Petri网的一种行为等价关系,最初在文献\cite{ABS91}中提出,并在\cite{Gor21}中被证明为可判定的。本文将其扩展至含有静默动作的有限Petri网,基于分支互模拟性\cite{vGW96}在带标签变迁系统上的直觉,提出了{\em 分支}位置互模拟性$\approx_p$。此外,我们遵循\cite{Gor21}中d-位置互模拟性的思想,提出了一个稍粗的变体,称为分支{\em d-位置}互模拟性$\approx_d$。我们证明了$\approx_p$和$\approx_d$是可判定的等价关系。进一步地,我们证明$\approx_d$严格细于分支全并发互模拟性\cite{Pin93,Gor20c},这主要是因为$\approx_d$不将那些预设规模大于1(即由多方交互产生的)的$\tau$标记网变迁视为不可观测行为。