2025/06/13 by Roberto Gorrieri, Gorrieri, Roberto, Ivan Lanese +1
Computer Science · Social Sciences · #68Q85 #Access Control and Trust #D.2.4 #F.1.1 #F.3.1 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Petri Nets in System Modeling
paper · pdf · doi:10.48550/arxiv.2506.11517
openalex publication_date 2025/06/13 · openalex created_date 2025/10/11 · openalex updated_date 2026/07/28
In the setting of Petri nets, we prove that \em causal-net bisimilarity \citeG15,Gor22,Gor25a, which is a refinement of history-preserving bisimilarity \citeRT88,vGG89,DDM89, and the novel \em hereditary causal-net bisimilarity, which is a refinement of hereditary history-preserving bisimilarity \citeBed91,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 \citeG15,Gor25a, that is decidable on finite bounded Petri nets \citeCG21a. Moreover, place bisimilarity \citeABS91, that we prove to be finer than causal-net bisimilarity, is also reversible and it was proved decidable for finite Petri nets in \citeGor21decid,Gor25a. These results offer two decidable reversible behavioral equivalences in the true concurrency spectrum, which are alternative to the coarser hereditary history-preserving bisimilarity \citeBed91,JNW96, that, unfortunately, is undecidable even for safe Petri nets \citeJNS03.