On Computing Fixpoints in Well-Structured Regular Model Checking, with Applications to Lossy Channel Systems
On Computing Fixpoints in Well-Structured Regular Model Checking, with Applications to Lossy Channel Systems
复制标题
关于计算结构良好的常规模型检查中的不动点及其在有损信道系统中的应用
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
P. Schnoebelen
中科院分区：
文献类型：
--
作者：
C. Baier;N. Bertrand;P. Schnoebelen
证明了良拟序集上“向上守护”不动点表达式的一个一般有限收敛定理。这在结构良好的系统的常规模型检查中有直接的应用，其中一个主要问题是不动点计算的最终收敛。特别是，我们能够直接获得几个新的可判定性结果有损信道系统。
We prove a general finite convergence theorem for “upward-guarded" fixpoint expressions over a well-quasi-ordered set. This has immediate applications in regular model checking of well-structured systems, where a main issue is the eventual convergence of fixpoint computations. In particular, we are able to directly obtain several new decidability results on lossy channel systems.