Ensuring completeness of symbolic verification methods for infinite-state systems
Ensuring completeness of symbolic verification methods for infinite-state systems
复制标题
确保无限状态系统符号验证方法的完整性
DOI：
10.1016/s0304-3975(00)00105-5
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
B. Jonsson
中科院分区：
文献类型：
--
作者：
P. Abdulla;B. Jonsson
在过去的几年中，针对无限状态系统的自动验证的研究工作不断增加。对于不同类别的此类系统，例如混合自动机、数据独立系统、关系自动机、Petri 网和有损通道系统，这项研究产生了许多非常重要的算法。随着人们对该领域的兴趣不断增加，提取这些和相关结果背后的共同原则将变得非常重要。在本文中，我们将提出无限状态系统的一般模型，并描述此类系统可达性分析的标准算法。我们的贡献在于找到算法可以完全自动化的条件。我们执行向后可达性分析。使用迭代过程，我们连续生成可达到给定最终状态的所有状态集的更大近似值。我们考虑这些近似值是良好准序的系统类别，这意味着迭代过程总是终止。从这些一般终止条件开始，我们推导出几种可达性可判定的计算模型。其中许多模型都是文献中现有模型的扩展。使用众所周知的从安全属性到可达性属性的简化，我们可以使用我们的算法来决定无限状态系统的大类安全属性。我们方法的动机是建立用于验证无限状态系统的通用工具的长期愿望，这意味着我们应该采用适用于相当广泛的此类系统的原则。
Over the last few years there has been an increasing research effort directed towards the automatic verification of infinite state systems. For different classes of such systems, e.g., hybrid automata, data-independent systems, relational automata, Petri nets, and lossy channel systems, this research has resulted in numerous highly nontrivial algorithms. As the interest in this area increases, it will be important to extract common principles that underly these and related results. In this paper, we will present a general model of infinite-state systems, and describe a standard algorithm for reachability analysis of such systems. Our contribution consists in finding conditions under which the algorithm can be fully automated. We perform backward reachability analysis. Using an iterative procedure, we generate successively larger approximations of the set of all states from which a given final state is reachable. We consider classes of systems where these approximations are well quasi-ordered, implying that the iterative procedure always terminates. Starting from these general termination conditions, we derive several computations models for which reachability is decidable. Many of these models are extensions of those existing in the literature. Using a well-known reduction from safety properties to reachability properties, we can use our algorithm to decide large classes of safety properties for infinite-state systems. A motivation for our approach is the long-term desire to build general tools for verification of infinite-state systems, which implies that we should employ principles applicable across a rather wide range of such systems.