zbMATH — the first resource for mathematics

Decidability of LTL for vector addition systems with one zero-test. (English) Zbl 1348.68157
Delzanno, Giorgio (ed.) et al., Reachability problems. 5th international workshop, RP 2011, Genoa, Italy, September 28–30, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-24287-8/pbk). Lecture Notes in Computer Science 6945, 85-95 (2011).
Summary: We consider the class of Vector Addition Systems with one zero-test and we show that the model-checking problem for LTL is decidable thanks to a reduction to the computability of the cover and the decidability of reachability. Our proof uses the notion of increasing loop, that we refine to fit the non-standard monotony of our system.
For the entire collection see [Zbl 1223.68005].

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
03B25 Decidability of theories and sets of sentences
03B44 Temporal logic
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI