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.
Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets / Cesco A.; Gorrieri R.. - ELETTRONICO. - 3072:(2021), pp. 135-149. (Intervento presentato al convegno 22nd Italian Conference on Theoretical Computer Science, ICTCS 2021 tenutosi a Bologna, Italy nel September 13-15, 2021).
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 | 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.
