Forward Analysis for WSTS, Part III: Karp-Miller Trees

TL;DR

This paper extends the framework for forward reachability analysis of well-structured transition systems (WSTS) by introducing a generic Karp-Miller algorithm for very-WSTS, enabling coverability and LTL model checking.

Contribution

It develops a generic Karp-Miller algorithm for very-WSTS, allowing finite representation of coverability sets and decidability of LTL model checking under certain conditions.

Findings

Coverability sets of very-WSTS can be computed as finite ideal decompositions.

LTL model checking for very-WSTS is decidable under natural effectiveness assumptions.

Termination relies on a new notion of acceleration levels characterized by ordinal ranks.

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.