FORWARD ANALYSIS FOR WSTS, PART II: COMPLETE WSTS
We describe a simple, conceptual forward analysis procedure for infinity-complete WSTS G. This computes the so-called clover of a state. When G is the completion of a WSTS X, the clover in 6 is a finite description of the downward closure of the reachability set. We show that such completions are infinity-complete exactly when X is an omega(2)- WSTS, a new robust class of WSTS. We show that our procedure terminates in more cases than the generalized Karp-Miller procedure on extensions of Petri nets and on lossy channel systems. We characterize the WSTS where our procedure terminates as those that are clover-flattable. Finally, we apply this to well-structured counter systems.
completion clover verification well-structured transition systems cover dcpo