Model Checking Coverability Graphs of Vector Addition Systems

DOI10.1007/978-3-642-22993-0_13MaRDI QIDQ3088033zbMATH OpenOpenAlexFDO

Authors Michel Blockelet, Sylvain Schmitz

Publication date 17 August 2011

Published in Mathematical Foundations of Computer Science 2011 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-22993-0_13

zbMATH Keywords

complexitycoverability propertiesCTLvector addition systems

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Model checking vector addition systems with one zero-test
• scientific article; zbMATH DE number 4092784
• Demystifying Reachability in Vector Addition Systems
• scientific article; zbMATH DE number 1304329
• scientific article; zbMATH DE number 3878366
• scientific article; zbMATH DE number 1852156
• scientific article; zbMATH DE number 7407775
• The complexity of reachability in affine vector addition systems with states

Cited in

(20)

• Strategic reasoning with a bounded number of resources: the quest for tractability
• Coverability Is undecidable in one-dimensional pushdown vector addition systems with resets
• Catching a structural bug with a flower
• Coverability trees for Petri nets with unordered data
• Complexity hierarchies beyond elementary
• Expand, Enlarge, and Check for Branching Vector Addition Systems
• Model checking vector addition systems with one zero-test
• Forward analysis and model checking for trace bounded WSTS
• Forward analysis and model checking for trace bounded WSTS
• Decidability of LTL for vector addition systems with one zero-test
• On the coverability problem for pushdown vector addition systems in one dimension
• On selective unboundedness of VASS
• Unboundedness problems for languages of vector addition systems
• The virtues of idleness: a decidable fragment of resource agent logic
• Exhibition of a structural bug with wings
• On the complexity of resource-bounded logics
• The ideal view on Rackoff's coverability technique
• Dimension-minimality and primality of counter nets
• Separability in Büchi VASS and singly nonlinear systems of inequalities
• Knowing-how reasoning with budgets recasted: universal reachability problem on VASS

This page was built for publication: Model Checking Coverability Graphs of Vector Addition Systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3088033)