Decidability and complexity of Petri nets with unordered data

DOI10.1016/j.tcs.2011.05.007zbMath1231.68172OpenAlexW1992428614WikidataQ57831211 ScholiaQ57831211MaRDI QIDQ554219

Fernando Rosa-Velardo, David de Frutos-Escrig

Publication date: 29 July 2011

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2011.05.007

zbMATH Keywords

boundednessreachabilityPetri netswell-structured transition systemspure names

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Related Items

Model checking Petri nets with names using data-centric dynamic systems ⋮ Data and process resonance. Identifier soundness for models of information systems ⋮ From DB-nets to Coloured Petri Nets with Priorities ⋮ Correctness Notions for Petri Nets with Identifiers ⋮ Unnamed Item ⋮ SMT-based verification of data-aware processes: a model-theoretic approach ⋮ Ordinal recursive complexity of unordered data nets ⋮ Dynamic Networks of Timed Petri Nets ⋮ Multiset rewriting for the verification of depth-bounded processes with name binding ⋮ WQO dichotomy for 3-graphs ⋮ Petri nets with name creation for transient secure association ⋮ The ideal view on Rackoff's coverability technique ⋮ Coverability Trees for Petri Nets with Unordered Data ⋮ Decidability Border for Petri Nets with Data: WQO Dichotomy Conjecture ⋮ A Non-Deterministic Multiset Query Language ⋮ Soundness Verification of Data-Aware Process Models with Variable-to-Variable Conditions

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A classification of the expressive power of well-structured transition systems
• A calculus of mobile processes. I
• Mobile ambients
• Algorithmic analysis of programs with well quasi-ordered domains.
• On the Expressiveness of Mobile Synchronizing Petri Nets
• Cost Soundness for Priced Resource-Constrained Workflow Nets
• Decidability Problems in Petri Nets with Names and Replication
• Constraint-based automatic verification of abstract models of multithreaded programs
• Instance Deadlock: A Mystery behind Frozen Programs
• Forward Analysis for Petri Nets with Name Creation
• Revisiting Ackermann-Hardness for Lossy Counter Machines and Reset Petri Nets
• Forward Analysis for WSTS, Part II: Complete WSTS
• Petri Nets as Token Objects
• Applications and Theory of Petri Nets 2004
• Applications and Theory of Petri Nets 2005
• Well-structured transition systems everywhere!