Abstract | ||
---|---|---|
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. |
Year | DOI | Venue |
---|---|---|
2020 | 10.23638/LMCS-16(2:13)2020 | LOGICAL METHODS IN COMPUTER SCIENCE |
Keywords | DocType | Volume |
well-structured transition systems,Karp-Miller trees,model checking,coverability,ideals | Journal | 16 |
Issue | ISSN | Citations |
2 | 1860-5974 | 0 |
PageRank | References | Authors |
0.34 | 0 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Michael Blondin | 1 | 27 | 9.06 |
Alain Finkel | 2 | 55 | 4.77 |
Jean Goubault-Larrecq | 3 | 582 | 40.90 |