Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets

DOI10.46298/LMCS-19(4:37)2023MaRDI QIDQ6137873zbMATH OpenOpenAlexFDO

Authors Roberto Gorrieri

Publication date 16 January 2024

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2104.14856

zbMATH Keywords

decidabilitybehavioral equivalencestrue concurrencycausal-net bisimilarityfully-concurrent bisimilarityi-causal-net bisimilarity

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

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.

Recommendations

• Deciding true concurrency equivalences on safe, finite nets
• Deciding true concurrency equivalences on finite safe nets (preliminary report)
• scientific article; zbMATH DE number 2102771
• Undecidability of bisimilarity for Petri nets and some related problems
• scientific article; zbMATH DE number 1555184

Cites work

• scientific article; zbMATH DE number 17804 (Why is no real title available?)
• scientific article; zbMATH DE number 176758 (Why is no real title available?)
• scientific article; zbMATH DE number 1302047 (Why is no real title available?)
• scientific article; zbMATH DE number 4119653 (Why is no real title available?)
• A coalgebraic semantics for causality in Petri nets
• A study on team bisimulation and H-team bisimulation for BPP nets
• Branching processes of Petri nets
• CONCUR 2005 – Concurrency Theory
• Concurrent bisimulations in Petri nets
• Concurrent systems and inevitability
• Deciding true concurrency equivalences on safe, finite nets
• Generalized OM-bisimulation
• Interleaving vs True Concurrency: Some Instructive Security Examples
• Minimal transition systems for history-preserving bisimulation
• Nets, Terms and Formulas
• On the semantics of place/transition Petri nets
• Petri nets are monoids
• Revisiting causality, coalgebraically
• Sequential and concurrent behaviour in Petri net theory
• Structure preserving bisimilarity, supporting an operational Petri net semantics of CCSP
• The non-sequential behaviour of Petri nets
• Undecidability of bisimilarity for Petri nets and some related problems

This page was built for publication: Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6137873)