On selective unboundedness of VASS
From MaRDI portal
Publication:355513
Abstract: Numerous properties of vector addition systems with states amount to checking the (un)boundedness of some selective feature (e.g., number of reversals, run length). Some of these features can be checked in exponential space by using Rackoff's proof or its variants, combined with Savitch's theorem. However, the question is still open for many others, e.g., reversal-boundedness. In the paper, we introduce the class of generalized unboundedness properties that can be verified in exponential space by extending Rackoff's technique, sometimes in an unorthodox way. We obtain new optimal upper bounds, for example for place-boundedness problem, reversal-boundedness detection (several variants exist), strong promptness detection problem and regularity detection. Our analysis is sufficiently refined so as we also obtain a polynomial-space bound when the dimension is fixed.
Recommendations
- Unboundedness problems for languages of vector addition systems
- A multiparameter analysis of the boundedness problem for vector addition systems
- Some complexity bounds for problems concerning finite and 2-dimensional vector addition systems with states
- Polynomial vector addition systems with states
- Mixing coverability and reachability to analyze VASS with one zero-test
Cites work
- scientific article; zbMATH DE number 4024806 (Why is no real title available?)
- scientific article; zbMATH DE number 46872 (Why is no real title available?)
- scientific article; zbMATH DE number 3582425 (Why is no real title available?)
- scientific article; zbMATH DE number 1223710 (Why is no real title available?)
- scientific article; zbMATH DE number 1302047 (Why is no real title available?)
- scientific article; zbMATH DE number 1142308 (Why is no real title available?)
- scientific article; zbMATH DE number 2081100 (Why is no real title available?)
- scientific article; zbMATH DE number 1405652 (Why is no real title available?)
- scientific article; zbMATH DE number 2206109 (Why is no real title available?)
- scientific article; zbMATH DE number 3310089 (Why is no real title available?)
- A multiparameter analysis of the boundedness problem for vector addition systems
- A structure to decide reachability in Petri nets
- A unified approach for deciding the existence of certain petri net paths
- An Algorithm for the General Petri Net Reachability Problem
- An NP-complete number-theoretic problem
- An analysis of the nonemptiness problem for classes of reversal-bounded multicounter machines
- Bounds on Positive Integral Solutions of Linear Diophantine Equations
- Counter machines and verification problems.
- Decidability of LTL for vector addition systems with one zero-test
- Fast acceleration of ultimately periodic relations
- Lectures on Petri nets. 1: Basic models. Advances in Petri nets
- Mixing coverability and reachability to analyze VASS with one zero-test
- Model Checking Coverability Graphs of Vector Addition Systems
- Modelchecking counting properties of 1-safe nets with buffers in paraPSPACE
- ON YEN'S PATH LOGIC FOR PETRI NETS
- On Context-Free Languages
- On Yen’s Path Logic for Petri Nets
- On the complexity of the linear-time μ-calculus for Petri Nets
- On the reachability problem for 5-dimensional vector addition systems
- Parallel program schemata
- Petri nets and regular languages
- Reduction and covering of infinite reachability trees
- Relationships between nondeterministic and deterministic tape complexities
- Reversal-Bounded Counter Machines Revisited
- Reversal-Bounded Multicounter Machines and Their Decision Problems
- Reversal-bounded multipushdown machines
- Taming past LTL and flat counter systems
- The Reachability Problem for Vector Addition System with One Zero-Test
- The covering and boundedness problems for vector addition systems
- The residue of vector sets with applications to decidability problems in Petri nets
- Vector addition system reachability problem, a short self-contained proof
- Verifying programs with unreliable channels
- Well-structured transition systems everywhere!
Cited in
(9)- scientific article; zbMATH DE number 7559503 (Why is no real title available?)
- On the existence and computability of long-run average properties in probabilistic VASS
- On the complexity of resource-bounded logics
- scientific article; zbMATH DE number 7204383 (Why is no real title available?)
- Coverability trees for Petri nets with unordered data
- Coverability synthesis in parametric Petri nets
- Dimension-minimality and primality of counter nets
- Unboundedness problems for languages of vector addition systems
- Strategic reasoning with a bounded number of resources: the quest for tractability
This page was built for publication: On selective unboundedness of VASS
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q355513)
