On selective unboundedness of VASS
From MaRDI portal
Publication:355513
DOI10.1016/J.JCSS.2013.01.014zbMATH Open1285.68094arXiv1011.0217OpenAlexW2963878989MaRDI QIDQ355513FDOQ355513
Authors: Stéphane Demri 
Publication date: 24 July 2013
Published in: Journal of Computer and System Sciences (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1011.0217
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
exponential spaceplace boundedness problemregularity detection problemvector addition systems with states
Cites Work
- Title not available (Why is that?)
- Reversal-bounded multipushdown machines
- Relationships between nondeterministic and deterministic tape complexities
- Parallel program schemata
- Reversal-Bounded Multicounter Machines and Their Decision Problems
- On Context-Free Languages
- Reduction and covering of infinite reachability trees
- The covering and boundedness problems for vector addition systems
- Verifying programs with unreliable channels
- ON YEN'S PATH LOGIC FOR PETRI NETS
- Model Checking Coverability Graphs of Vector Addition Systems
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Well-structured transition systems everywhere!
- On the reachability problem for 5-dimensional vector addition systems
- A structure to decide reachability in Petri nets
- Title not available (Why is that?)
- Vector addition system reachability problem, a short self-contained proof
- Petri nets and regular languages
- On the complexity of the linear-time μ-calculus for Petri Nets
- An analysis of the nonemptiness problem for classes of reversal-bounded multicounter machines
- A unified approach for deciding the existence of certain petri net paths
- Lectures on Petri nets. 1: Basic models. Advances in Petri nets
- A multiparameter analysis of the boundedness problem for vector addition systems
- Counter machines and verification problems.
- Taming past LTL and flat counter systems
- Modelchecking counting properties of 1-safe nets with buffers in paraPSPACE
- The Reachability Problem for Vector Addition System with One Zero-Test
- Decidability of LTL for vector addition systems with one zero-test
- Mixing coverability and reachability to analyze VASS with one zero-test
- Fast acceleration of ultimately periodic relations
- Reversal-Bounded Counter Machines Revisited
- On Yen’s Path Logic for Petri Nets
- An Algorithm for the General Petri Net Reachability Problem
- Title not available (Why is that?)
- Bounds on Positive Integral Solutions of Linear Diophantine Equations
- Title not available (Why is that?)
- An NP-complete number-theoretic problem
- The residue of vector sets with applications to decidability problems in Petri nets
Cited In (9)
- Title not available (Why is that?)
- On the complexity of resource-bounded logics
- On the existence and computability of long-run average properties in probabilistic VASS
- Title not available (Why is that?)
- 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
Uses Software
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)
