Decidable Reversible Equivalences for Finite Petri Nets
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866912428270288896 |
|---|---|
| author | Gorrieri, Roberto Lanese, Ivan |
| author_facet | Gorrieri, Roberto Lanese, Ivan |
| contents | 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}. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_11517 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Decidable Reversible Equivalences for Finite Petri Nets Gorrieri, Roberto Lanese, Ivan Logic in Computer Science 68Q85 F.1.1; D.2.4; F.3.1 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}. |
| title | Decidable Reversible Equivalences for Finite Petri Nets |
| topic | Logic in Computer Science 68Q85 F.1.1; D.2.4; F.3.1 |
| url | https://arxiv.org/abs/2506.11517 |