Sciweavers

Share
ICALP
2009
Springer

Forward Analysis for WSTS, Part II: Complete WSTS

12 years 12 months ago
Forward Analysis for WSTS, Part II: Complete WSTS
Abstract. We describe a simple, conceptual forward analysis procedure for complete WSTS S. This computes the clover of a state s0, i.e., a finite description of the closure of the cover of s0. When S is the completion of a WSTS X, the clover in S is a finite description of the cover in X. We show that this applies exactly when X 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.
Alain Finkel, Jean Goubault-Larrecq
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2009
Where ICALP
Authors Alain Finkel, Jean Goubault-Larrecq
Comments (0)
books