Reachability in vector addition systems is primitive-recursive in fixed dimension

DOI10.5555/3470152.3470202MaRDI QIDQ6654515zbMATH OpenFDO

Authors Jérôme Leroux, Sylvain Schmitz

Publication date 19 December 2024

Full work available at URL https://doi.org/10.5555/3470152.3470202

zbMATH Keywords

fast-growing complexityPetri netreachabilityvector addition system

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cited in

(28)

• Nominal tree automata with name allocation
• On continuous pushdown VASS in one dimension
• Bi-reachability in Petri nets with data
• Invariants for one-counter automata with disequality tests
• Verification of population protocols with unordered data
• Improved algorithm for reachability in d-VASS
• Structural liveness of conservative Petri nets
• Coverability in VASS revisited: improving Rackoff's bounds to obtain conditional optimality
• Counter machines with infrequent reversals
• New lower bounds for reachability in vector addition systems
• Acyclic Petri and workflow nets with resets
• The semilinear home-space problem is Ackermann-complete for Petri nets
• Monus semantics in vector addition systems with states
• Geometry of reachability sets of vector addition systems
• On the separability problem of VASS reachability languages
• Soundness of reset workflow nets
• The geometry of reachability in continuous vector addition systems with states
• Language inclusion for boundedly-ambiguous vector addition systems is decidable
• On the home-space problem for Petri nets and its Ackermannian complexity
• Challenges of the reachability problem in infinite-state systems (invited paper)
• Improved lower bounds for reachability in vector addition systems
• Knowing-how reasoning with budgets recasted: universal reachability problem on VASS
• On the reachability problem for two-dimensional branching VASS
• Wait-only broadcast protocols are easier to verify
• Reachability in symmetric VASS
• Reachability in vector addition system with states parameterized by geometric dimension
• Bridging the gap between plain VASS and branching VASS
• A note on the parameterised complexity of coverability in vector addition systems

This page was built for publication: Reachability in vector addition systems is primitive-recursive in fixed dimension

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