Alain Finkel ; Jean Goubault-Larrecq - Forward Analysis for WSTS, Part II: Complete WSTS

lmcs:1217 - Logical Methods in Computer Science, September 29, 2012, Volume 8, Issue 3 - https://doi.org/10.2168/LMCS-8(3:28)2012
Forward Analysis for WSTS, Part II: Complete WSTSArticle

Authors: 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 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.


    Volume: Volume 8, Issue 3
    Published on: September 29, 2012
    Imported on: November 24, 2009
    Keywords: Computer Science - Logic in Computer Science,D.2.4, F.3.1

    14 Documents citing this article

    Consultation statistics

    This page has been seen 1145 times.
    This article's PDF has been downloaded 310 times.