Decidable Reversible Equivalences for Finite Petri Nets

TL;DR

This paper proves that certain reversible behavioral equivalences for finite Petri nets are decidable, providing new tools for analyzing concurrent systems with reversible behaviors.

Contribution

It establishes the decidability of causal-net bisimilarity and place bisimilarity as reversible equivalences for finite Petri nets, refining prior undecidable relations.

Findings

Causal-net bisimilarity coincides with hereditary causal-net bisimilarity.

Both causal-net and place bisimilarity are decidable and reversible.

Hereditary history-preserving bisimilarity remains undecidable for safe 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}.