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

complexityCTLvector addition systemscoverability properties

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

(18)

• Decidability of LTL for vector addition systems with one zero-test
• Model checking vector addition systems with one zero-test
• On the complexity of resource-bounded logics
• Forward analysis and model checking for trace bounded WSTS
• Coverability trees for Petri nets with unordered data
• Forward analysis and model checking for trace bounded WSTS
• On the coverability problem for pushdown vector addition systems in one dimension
• Catching a structural bug with a flower
• The ideal view on Rackoff's coverability technique
• 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
• Separability in Büchi VASS and singly nonlinear systems of inequalities
• On selective unboundedness of VASS
• Expand, Enlarge, and Check for Branching Vector Addition Systems
• Complexity hierarchies beyond elementary
• The virtues of idleness: a decidable fragment of resource agent logic
• Exhibition of a structural bug with wings

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)