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 WSTS

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
    Accepted on: June 25, 2015
    Submitted on: November 24, 2009
    Keywords: Computer Science - Logic in Computer Science,D.2.4, F.3.1

    Linked data

    Source : ScholeXplorer IsReferencedBy ARXIV 1402.2908
    Source : ScholeXplorer IsReferencedBy DOI 10.1007/978-3-642-40184-8_2
    Source : ScholeXplorer IsReferencedBy DOI 10.48550/arxiv.1402.2908
    • 1402.2908
    • 10.48550/arxiv.1402.2908
    • 10.1007/978-3-642-40184-8_2
    • 10.1007/978-3-642-40184-8_2
    • 10.1007/978-3-642-40184-8_2
    The Power of Well-Structured Systems
    Schmitz, Sylvain ; Schnoebelen, Philippe ;

    13 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 419 times.
    This article's PDF has been downloaded 230 times.