Demystifying Reachability in Vector Addition Systems

DOI10.1109/LICS.2015.16zbMATH Open1392.68308arXiv1503.00745MaRDI QIDQ4635791FDOQ4635791

Jérôme Leroux, Sylvain Schmitz

Publication date: 23 April 2018

Published in: 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Abstract: More than 30 years after their inception, the decidability proofs for reachability in vector addition systems (VAS) still retain much of their mystery. These proofs rely crucially on a decomposition of runs successively refined by Mayr, Kosaraju, and Lambert, which appears rather magical, and for which no complexity upper bound is known. We first offer a justification for this decomposition technique, by showing that it computes the ideal decomposition of the set of runs, using the natural embedding relation between runs as well quasi ordering. In a second part, we apply recent results on the complexity of termination thanks to well quasi orders and well orders to obtain a cubic Ackermann upper bound for the decomposition algorithms, thus providing the first known upper bounds for general VAS reachability.

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

Recommendations

• scientific article; zbMATH DE number 3878366
• scientific article
• Vector addition system reachability problem: a short self-contained proof
• Vector addition system reachability problem, a short self-contained proof
• scientific article; zbMATH DE number 7559504
• Vector addition system reversible reachability problem
• Vector Addition System Reversible Reachability Problem
• Separability of reachability sets of vector addition systems
• The complexity of reachability in affine vector addition systems with states
• scientific article; zbMATH DE number 7407775

zbMATH Keywords

computational complexitydecidabilityPetri netsreachability analysisprogram verification

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)

Cited In (41)

• Reachability problems on reliable and lossy queue automata
• Title not available (Why is that?)
• Title not available (Why is that?)
• On the decision problem for MELL
• Deciding Structural Liveness of Petri Nets
• Zeno, Hercules, and the Hydra
• On the complexity of resource-bounded logics
• A lazy query scheme for reachability analysis in Petri nets
• Flat Petri nets (invited talk)
• On Freeze LTL with Ordered Attributes
• Unboundedness problems for machines with reversal-bounded counters
• Extensional Petri net
• Directed reachability for infinite-state systems
• A counter abstraction technique for verifying properties of probabilistic swarm systems
• The Ideal Approach to Computing Closed Subsets in Well-Quasi-orderings
• Forward analysis for WSTS, part I: completions
• Reasoning about reversal-bounded counter machines
• Context-free commutative grammars with integer counters and resets
• Petri Nets and Semilinear Sets (Extended Abstract)
• The Reachability Problem for Vector Addition System with One Zero-Test
• A Note on C² Interpreted over Finite Data-Words
• Title not available (Why is that?)
• Title not available (Why is that?)
• Coverability Trees for Petri Nets with Unordered Data
• Title not available (Why is that?)
• Title not available (Why is that?)
• Ackermannian completion of separators
• Reachability in fixed VASS: expressiveness and lower bounds
• Solvability of orbit-finite systems of linear equations
• The complexity of soundness in workflow nets
• Vector Addition System Reversible Reachability Problem
• Shortest Paths in One-Counter Systems
• A Relational Trace Logic for Vector Addition Systems with Application to Context-Freeness
• Expand, Enlarge, and Check for Branching Vector Addition Systems
• Handling infinitely branching well-structured transition systems
• Open Petri nets
• Title not available (Why is that?)
• Complexity hierarchies beyond elementary
• Infinitary Noetherian constructions I. Infinite words
• Model Checking Coverability Graphs of Vector Addition Systems
• Verification of population protocols

This page was built for publication: Demystifying Reachability in Vector Addition Systems

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