We prove that the well-known (strong) fully-concurrent bisimilarity and the novel i-causal-net bisimilarity, which is a sligtlhy coarser variant of causal-net bisimilarity, are decidable for finite bounded Petri nets. The proofs are based on a generalization of the ordered marking proof technique that Vogler used to demonstrate that (strong) fully-concurrent bisimilarity (or, equivalently, history-preserving bisimilarity) is decidable on finite safe nets.
Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets / Cesco, Arnaldo; Gorrieri, Roberto. - In: LOGICAL METHODS IN COMPUTER SCIENCE. - ISSN 1860-5974. - ELETTRONICO. - 19:4(2023), pp. 1-37. [10.46298/lmcs-19(4:37)2023]
Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets
Gorrieri, Roberto
2023
Abstract
We prove that the well-known (strong) fully-concurrent bisimilarity and the novel i-causal-net bisimilarity, which is a sligtlhy coarser variant of causal-net bisimilarity, are decidable for finite bounded Petri nets. The proofs are based on a generalization of the ordered marking proof technique that Vogler used to demonstrate that (strong) fully-concurrent bisimilarity (or, equivalently, history-preserving bisimilarity) is decidable on finite safe nets.| File | Dimensione | Formato | |
|---|---|---|---|
|
2104.14856.pdf
accesso aperto
Descrizione: file editoriale
Tipo:
Versione (PDF) editoriale
Licenza:
Licenza per Accesso Aperto. Creative Commons Attribuzione (CCBY)
Dimensione
570.95 kB
Formato
Adobe PDF
|
570.95 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
