We describe a simple, conceptual forward analysis procedure for ∞-complete WSTS . This computes the clover of a state s 0, i.e., a finite description of the closure of the cover of s 0. When is the completion of a WSTS , the clover in is a finite description of the cover in . We show that this applies exactly when is an ω 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. We characterize the WSTS where our procedure terminates as those that are clover-flattable. Finally, we apply this to well-structured counter systems. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Finkel, A., & Goubault-Larrecq, J. (2009). Forward analysis for WSTS, part II: Complete WSTS. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5556 LNCS, pp. 188–199). https://doi.org/10.1007/978-3-642-02930-1_16
Mendeley helps you to discover research relevant for your work.