Decidable Reversible Equivalences for Finite Petri Nets

Abstract

In the setting of Petri nets, we prove that {\em causal-net bisimilarity} \cite{G15,Gor22,Gor25a}, which is a refinement of history-preserving bisimilarity \cite{RT88,vGG89,DDM89}, and the novel {\em hereditary} causal-net bisimilarity, which is a refinement of hereditary history-preserving bisimilarity \cite{Bed91,JNW96}, do coincide. This means that causal-net bisimilarity is a {\em reversible behavioral equivalence}, as causal-net bisimilar markings not only are able to match each other's forward transitions, but also backward transitions by undoing performed events. Causal-net bisimilarity can be equivalently formulated as {\em structure-preserving bisimilarity} \cite{G15,Gor25a}, that is decidable on finite bounded Petri nets \cite{CG21a}. Moreover, place bisimilarity \cite{ABS91}, that we prove to be finer than causal-net bisimilarity, is also reversible and it was proved decidable for finite Petri nets in \cite{Gor21decid,Gor25a}. These results offer two decidable reversible behavioral equivalences in the true concurrency spectrum, which are alternative to the coarser hereditary history-preserving bisimilarity \cite{Bed91,JNW96}, that, unfortunately, is undecidable even for safe Petri nets \cite{JNS03}.