On selective unboundedness of VASS
From MaRDI portal
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
- 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 analysis of the nonemptiness problem for classes of reversal-bounded multicounter machines
- An NP-complete number-theoretic problem
- 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
- 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?)
- 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 Context-Free Languages
- On the complexity of the linear-time μ-calculus for Petri Nets
- On the reachability problem for 5-dimensional vector addition systems
- ON YEN'S PATH LOGIC FOR PETRI NETS
- On Yen’s Path Logic for Petri Nets
- 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 covering and boundedness problems for vector addition systems
- The Reachability Problem for Vector Addition System with One Zero-Test
- 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
(14)- Strategic reasoning with a bounded number of resources: the quest for tractability
- Coverability trees for Petri nets with unordered data
- On the existence and computability of long-run average properties in probabilistic VASS
- Unboundedness problems for languages of vector addition systems
- scientific article; zbMATH DE number 7559503 (Why is no real title available?)
- scientific article; zbMATH DE number 7204383 (Why is no real title available?)
- Coverability synthesis in parametric Petri nets
- On the complexity of resource-bounded logics
- Dimension-minimality and primality of counter nets
- Separability in Büchi VASS and singly nonlinear systems of inequalities
- About decisiveness of dynamic probabilistic models
- On the separability problem of VASS reachability languages
- Box-reachability in vector addition systems
- Knowing-how reasoning with budgets recasted: universal reachability problem on VASS
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)
