Résumé | We design a variation of the Karp-Miller algorithm to compute a
finite representation of the cover (i.e., the downward closure of
the reachability set) of a vector addition system with one
zero-test. This algorithm yields decision procedures for several
problems on these systems, open until now, such as
place-boundedness or LTL model-checking.
The proof techniques to handle the zero-test are based on two new
notions of cover: the refined and the filtered cover. The refined
cover is hybrid between the reachability set and the classical
cover. It inherits properties of the reachability set: equality
of two refined covers is undecidable, even for usual Vector
Addition Systems (with no zero-test), but the refined cover of a
Vector Addition System is a recursive set. The second notion of
cover, called the filtered cover, is the central tool of our
algorithms. It inherits properties of the classical cover, and in
particular, one can effectively compute a finite representation
of this set, even for Vector Addition Systems with one zero-test. |