2026-07-19T18:02:08Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:8403 2024-03-06T10:41:56Z ddc:004 open_access

Forward Analysis for WSTS, Part III: Karp-Miller Trees Blondin, Michael Finkel, Alain Goubault-Larrecq, Jean WSTS model checking coverability Karp-Miller algorithm ideals 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 downwards-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 assumptions on positive sequences, 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Michael Blondin and Alain Finkel and Jean Goubault-Larrecq 2018 Is Part Of LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2017.16 urn:nbn:de:0030-drops-84033 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.16 eng https://creativecommons.org/licenses/by/3.0/legalcode