Unboundedness problems for languages of vector addition systems
From MaRDI portal
Abstract: A vector addition system (VAS) with an initial and a final marking and transition labels induces a language. In part because the reachability problem in VAS remains far from being well-understood, it is difficult to devise decision procedures for such languages. This is especially true for checking properties that state the existence of infinitely many words of a particular shape. Informally, we call these emph{unboundedness properties}. We present a simple set of axioms for predicates that can express unboundedness properties. Our main result is that such a predicate is decidable for VAS languages as soon as it is decidable for regular languages. Among other results, this allows us to show decidability of (i)~separability by bounded regular languages, (ii)~unboundedness of occurring factors from a language with mild conditions on , and (iii)~universality of the set of factors.
Recommendations
- On selective unboundedness of VASS
- On boundedness problems for pushdown vector addition systems
- Some complexity bounds for problems concerning finite and 2-dimensional vector addition systems with states
- On the context-freeness problem for vector addition systems
- The general vector addition system reachability problem by Presburger inductive invariants
Cites work
- A characterization for decidable separability by piecewise testable languages
- A Characterization of Semilinear Sets
- A Generic Approach to the Static Analysis of Concurrent Programs with Procedures
- A perfect model for bounded verification
- A structure to decide reachability in Petri nets
- A unified approach for deciding the existence of certain petri net paths
- An approach to computing downward closures
- Approximating Petri net reachability along context-free traces
- Bounded Algol-Like Languages
- Bounded Regular Sets
- Bounded underapproximations
- Complexity of pattern-based verification for multithreaded programs
- Concatenation hierarchies: new bottle, old wine
- Deciding piecewise testable separability for regular tree languages
- Finding the growth rate of a regular or context-free language in polynomial time
- Forward analysis and model checking for trace bounded WSTS
- scientific article; zbMATH DE number 3660804 (Why is no real title available?)
- scientific article; zbMATH DE number 3664335 (Why is no real title available?)
- scientific article; zbMATH DE number 3628412 (Why is no real title available?)
- It is Undecidable if Two Regular Tree Languages can be Separated by a Deterministic Tree-walking Automaton
- Model Checking Coverability Graphs of Vector Addition Systems
- Model-checking \(\mathrm{CTL}^*\) over flat Presburger counter systems
- On free monoids partially ordered by embedding
- On the coverability problem for pushdown vector addition systems in one dimension
- ON YEN'S PATH LOGIC FOR PETRI NETS
- Ordering by Divisibility in Abstract Algebras
- Petri net algorithms in the theory of matrix grammars
- Place-boundedness for vector addition systems with one zero-test
- Reachability in Petri nets with inhibitor arcs
- Regular cost functions. I: Logic and algebra over words
- Regular separability of one counter automata
- Regular separability of Parikh automata
- Remarks on blind and partially blind one-way multicounter machines
- Separability of reachability sets of vector addition systems
- Separation for dot-depth two
- The downward-closure of Petri net languages
- The emptiness problem for valence automata over graph monoids
- Tools and Algorithms for the Construction and Analysis of Systems
- Well-structured languages
Cited in
(10)- A note on fine covers and iterable factors of VAS languages
- Reachability problems in low-dimensional nondeterministic polynomial maps over integers
- On selective unboundedness of VASS
- On the context-freeness problem for vector addition systems
- Unboundedness problems for machines with reversal-bounded counters
- Relativized codes, finite decodability, and bounded languages
- Separability in Büchi VASS and singly nonlinear systems of inequalities
- Separability and non-determinizability of WSTS
- Verifying unboundedness via amalgamation
- Techniques for showing the decidability of the boundedness problem of language acceptors
This page was built for publication: Unboundedness problems for languages of vector addition systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5002804)
