Michael Blondin ; Alain Finkel ; Jean Goubault-Larrecq - Forward Analysis for WSTS, Part III: Karp-Miller Trees

lmcs:4971 - Logical Methods in Computer Science, June 23, 2020, Volume 16, Issue 2 - https://doi.org/10.23638/LMCS-16(2:13)2020
Forward Analysis for WSTS, Part III: Karp-Miller TreesArticle

Authors: Michael Blondin ; Alain Finkel ; Jean Goubault-Larrecq

    This paper is a sequel of "Forward Analysis for WSTS, Part I: Completions" [STACS 2009, LZI Intl. Proc. in Informatics 3, 433-444] and "Forward Analysis for WSTS, Part II: Complete WSTS" [Logical Methods in Computer Science 8(3), 2012]. In these two papers, we provided a framework to conduct forward reachability analyses of WSTS, using finite representations of downward-closed sets. We further develop this framework to obtain a generic Karp-Miller algorithm for the new class of very-WSTS. This allows us to show that coverability sets of very-WSTS can be computed as their finite ideal decompositions. Under natural effectiveness assumptions, we also show that LTL model checking for very-WSTS is decidable. The termination of our procedure rests on a new notion of acceleration levels, which we study. We characterize those domains that allow for only finitely many accelerations, based on ordinal ranks.


    Volume: Volume 16, Issue 2
    Published on: June 23, 2020
    Accepted on: May 12, 2020
    Submitted on: November 15, 2018
    Keywords: Computer Science - Logic in Computer Science,F.1.1,F.3.1
    Funding:
      Source : OpenAIRE Graph
    • Funder: Natural Sciences and Engineering Research Council of Canada

    1 Document citing this article

    Consultation statistics

    This page has been seen 1199 times.
    This article's PDF has been downloaded 334 times.