Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets

DOI10.46298/LMCS-19(4:37)2023arXiv2104.14856OpenAlexW3158514776MaRDI QIDQ6137873FDOQ6137873

Roberto Gorrieri, Author name not available (Why is that?)

Publication date: 16 January 2024

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

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.

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)

Cites Work

• Concurrent bisimulations in Petri nets
• Title not available (Why is that?)
• Title not available (Why is that?)
• The non-sequential behaviour of Petri nets
• Title not available (Why is that?)
• Branching processes of Petri nets
• Minimal transition systems for history-preserving bisimulation
• Nets, Terms and Formulas
• Undecidability of bisimilarity for Petri nets and some related problems
• Sequential and concurrent behaviour in Petri net theory
• Petri nets are monoids
• Generalized OM-bisimulation
• Deciding true concurrency equivalences on safe, finite nets
• Title not available (Why is that?)
• CONCUR 2005 – Concurrency Theory
• On the semantics of place/transition Petri nets
• Revisiting causality, coalgebraically
• A coalgebraic semantics for causality in Petri nets
• Concurrent systems and inevitability
• Structure Preserving Bisimilarity, Supporting an Operational Petri Net Semantics of CCSP
• A study on team bisimulation and H-team bisimulation for BPP nets
• Interleaving vs True Concurrency: Some Instructive Security Examples

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)