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.

翻译：本文是“WSTS前期分析,第一部分:完成”[STACS 2009, LZI Intl. proc., 信息学, 3, 433-4444] 和“WSTS前期分析, 第二部分: 完整的WSTS” [计算机科学8(3), 2012] 的续 。 在这两份文件中,我们提供了一个框架,用于对WSTS进行前期可达性分析, 使用自下而上封闭的数据集的有限表示。 我们进一步开发了这个框架, 以获得新类的非常WSTS通用的卡普- 米勒算法。 这使我们能够显示, 能够将非常WSTS的可覆盖性组合计算为有限的理想分解。 在自然有效性假设下, 我们还显示, 对非常WSTSTS的 LTL 模式检查是可以确定的。 我们程序的终止取决于一个新的加速度概念, 我们研究这个概念。 我们用恒定了那些区域, 仅允许以恒定数量的速度, 以星级为基础, 。