We consider the class of Vector Addition Systems with one zero-test and we show that the model-checking problem for LTL is de-cidable 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.
展开▼
