2 results
Rémi Bonnet ; Alain FInkel ; Jérôme Leroux ; Marc Zeitoun.
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 vector addition system with one zero-test. This algorithm yields decision procedures for several problems for these […]
Published on June 19, 2012
Alain Finkel ; Jean Goubault-Larrecq.
We describe a simple, conceptual forward analysis procedure for infinity-complete WSTS S. This computes the so-called clover of a state. When S is the completion of a WSTS X, the clover in S is a finite description of the downward closure of the reachability set. We show that such completions are […]
Published on September 29, 2012