WSTS 的前向分析，第二部分：完备 WSTS

我们描述了一种针对无穷完备 WSTS $S$ 的简单概念性前向分析过程。该过程计算所谓的状态 clover。当$S$是 WSTS $X$ 的完备化时，$S$中的 clover 是可到达集向下闭包的一个有限描述。我们证明，此类完备化是无穷完备的，当且仅当$X$是一个$\omega$-2-WSTS，这是一类新的鲁棒 WSTS。我们表明，我们的过程在比扩展 Petri 网和有损信道系统上的广义 Karp-Miller 过程更多的情况下终止。我们将我们的过程能终止的 WSTS 刻画为那些 clover-可扁平化的系统。最后，我们将此应用于良结构计数器系统。