Model Checking Vector Addition Systems with one zero-test

Rémi Bonnet, Alain FInkel, Jérôme Leroux +1

We design a variation of the Karp-Miller algorithm to compute, in a forward manner, a finite representation of the cover (i.e., the downward closure of the reachability set) of a v…