一句话：为 very-WSTS 提出通用 Karp-Miller 算法，可计算覆盖集并判定 LTL 模型检测。
本文延续 WSTS 前向分析系列工作，研究如何对良结构迁移系统（WSTS）进行前向可达性与覆盖性分析，并将已有基于向下封闭集有限表示的框架推广到新类 very-WSTS。作者提出通用的 Karp-Miller 算法，证明 very-WSTS 的覆盖集可计算为有限的理想分解；算法终止性依赖于新引入的加速层级概念，并通过序数秩刻画哪些域仅允许有限次加速。在自然的有效性假设下，论文还证明 very-WSTS 的 LTL 模型检测是可判定的。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{BlondinFG20,
title = {Forward Analysis for WSTS, Part III: Karp-Miller Trees},
author = {Michael Blondin and Alain Finkel and Jean Goubault-Larrecq},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 2},
year = {2020},
doi = {10.23638/lmcs-16(2:13)2020}
}