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

DOI10.1007/978-3-662-47666-6_26zbMATH Open1440.68177arXiv1503.04018OpenAlexW1506909315MaRDI QIDQ3449486FDOQ3449486

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)

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.

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

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

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)

Cites Work

• Semigroups, Presburger formulas, and languages
• The covering and boundedness problems for vector addition systems
• Reachability in Two-Dimensional Vector Addition Systems with States Is PSPACE-Complete
• CONCUR 2004 - Concurrency Theory
• Vector addition system reachability problem
• Automatic verification of recursive procedures with one integer parameter.
• Reachability in Petri Nets with Inhibitor Arcs
• Approximating Petri net reachability along context-free traces
• Nonelementary Complexities for Branching VASS, MELL, and Extensions
• The covering and boundedness problems for branching vector addition systems
• Hyper-Ackermannian bounds for pushdown vector addition systems
• Alternating Vector Addition Systems with States
• On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension

Cited In (13)

• Unboundedness Problems for Languages of Vector Addition Systems.
• A lower bound for the coverability problem in acyclic pushdown VAS
• On the Boundedness Problem for Higher-Order Pushdown Vector Addition Systems
• The emptiness problem for valence automata over graph monoids
• Title not available (Why is that?)
• On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension
• Hyper-Ackermannian bounds for pushdown vector addition systems
• Coverability in 2-VASS with one unary counter is in NP
• The complexity of bidirected reachability in valence systems
• The context-freeness of the languages associated with vector addition systems is decidable
• Title not available (Why is that?)
• Recent advances on reachability problems for valence systems (invited talk)
• Title not available (Why is that?)

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)