Forward Analysis for WSTS, Part II: Complete WSTS

We describe a simple, conceptual forward analysis procedure forinfinity-complete WSTS S. This computes the so-called clover of a state. When Sis the completion of a WSTS X, the clover in S is a finite description of thedownward closure of the reachability set. We show that such completions areinfinity-complete exactly when X is an omega-2-WSTS, a new robust class ofWSTS. We show that our procedure terminates in more cases than the generalizedKarp-Miller procedure on extensions of Petri nets and on lossy channel systems.We characterize the WSTS where our procedure terminates as those that areclover-flattable. Finally, we apply this to well-structured counter systems.Comment: 35 pages, 6 figures. An extended abstract already appeared in Proc. 36th Intl. Coll. Automata, Languages and Programming (ICALP'09