We prove that (strong) fully-concurrent bisimilarity and 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, historypreserving bisimilarity) is decidable on finite safe nets.
Cesco A., Gorrieri R. (2021). Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets. CEUR-WS.
Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets
Cesco A.
;Gorrieri R.
2021
Abstract
We prove that (strong) fully-concurrent bisimilarity and 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, historypreserving bisimilarity) is decidable on finite safe nets.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
paper12.pdf
accesso aperto
Tipo:
Versione (PDF) editoriale
Licenza:
Licenza per Accesso Aperto. Creative Commons Attribuzione (CCBY)
Dimensione
407.15 kB
Formato
Adobe PDF
|
407.15 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
