Branching Place Bisimilarity: A Decidable Behavioral Equivalence for Finite Petri Nets with Silent Moves

Place bisimilarity ∼p is a behavioral equivalence for finite Petri nets, proposed in [1] and proved decidable in [13]. In this paper we propose an extension to finite Petri nets with silent moves of the place bisimulation idea, yielding branching place bisimilarity ≈p, following the intuition of branching bisimilarity [6] on labeled transition systems. We prove that ≈p is a decidbale equivalence relation. Moreover, we argue that it is strictly finer than branching fully-concurrent bisimilarity [12, 22], essentially because ≈p does not consider as unobservable those τ -labeled net transitions with pre-set size larger than one, i.e., those resulting from multi-party interaction.