On the coverability problem for pushdown vector addition systems in one dimension

DOI10.1007/978-3-662-47666-6_26MaRDI QIDQ3449486zbMATH OpenOpenAlexFDO

Authors Jérôme Leroux, Grégoire Sutre, Patrick Totzke

Publication date 4 November 2015

Published in Automata, Languages, and Programming (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: Does the trace language of a given vector addition system (VAS) intersect with a given context-free language? This question lies at the heart of several verification questions involving recursive programs with integer parameters. In particular, it is equivalent to the coverability problem for VAS that operate on a pushdown stack. We show decidability in dimension one, based on an analysis of a new model called grammar-controlled vector addition systems.

Recommendations

• On boundedness problems for pushdown vector addition systems
• On the context-freeness problem for vector addition systems
• The context-freeness of the languages associated with vector addition systems is decidable
• Well-structured pushdown systems
• Model Checking Coverability Graphs of Vector Addition Systems

Cites work

• Alternating vector addition systems with states
• Approximating Petri net reachability along context-free traces
• Automatic verification of recursive procedures with one integer parameter.
• CONCUR 2004 - Concurrency Theory
• Hyper-Ackermannian bounds for pushdown vector addition systems
• On the coverability problem for pushdown vector addition systems in one dimension
• Reachability in Petri nets with inhibitor arcs
• Reachability in two-dimensional vector addition systems with states is PSPACE-complete
• Semigroups, Presburger formulas, and languages
• The covering and boundedness problems for branching vector addition systems
• The covering and boundedness problems for vector addition systems
• Vector addition system reachability problem, a short self-contained proof

Cited in

(15)

• On functions weakly computable by pushdown Petri nets and related systems
• On the coverability problem for pushdown vector addition systems in one dimension
• A lower bound for the coverability problem in acyclic pushdown VAS
• On the Boundedness Problem for Higher-Order Pushdown Vector Addition Systems
• On the context-freeness problem for vector addition systems
• The emptiness problem for valence automata over graph monoids
• scientific article; zbMATH DE number 7559493 (Why is no real title available?)
• Unboundedness problems for languages of vector addition systems
• On boundedness problems for pushdown vector addition systems
• Hyper-Ackermannian bounds for pushdown vector addition systems
• The context-freeness of the languages associated with vector addition systems is decidable
• Coverability in 2-VASS with one unary counter is in NP
• The complexity of bidirected reachability in valence systems
• scientific article; zbMATH DE number 7559504 (Why is no real title available?)
• Recent advances on reachability problems for valence systems (invited talk)

This page was built for publication: On the coverability problem for pushdown vector addition systems in one dimension

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