From Pre-Historic to Post-Modern Symbolic Model Checking
From Pre-Historic to Post-Modern Symbolic Model Checking
复制标题
从史前到后现代的符号模型检查
DOI：
--
复制
发表时间：
1998
期刊：
影响因子：
--
通讯作者：
S. Qadeer
中科院分区：
文献类型：
--
作者：
T. Henzinger;O. Kupferman;S. Qadeer
符号模型检查能够自动验证大型系统，它通过计算表示状态集的表达式来进行。传统上，符号模型检查工具是基于向后状态遍历的；它们的基本操作是函数pre，给定一组状态后，该函数返回所有先前状态的集合。这是因为说明符通常使用具有未来时间模式的形式，这些模式自然是通过迭代pre的应用程序来评估的。实验表明，如果符号模型检查是基于前向状态遍历的，那么它的性能会显著提高；在本例中，基本操作是post函数，它在给定一组状态后返回所有后续状态的集合。这是因为前向状态遍历可以确保只有从初始状态可到达且与满足或违反规范相关的部分状态空间被探索；也就是说，可以尽快检测到错误。在本文中，我们研究了哪些规范可以通过符号前向状态遍历进行检查。利用两μ-演算的方法，给出了符号前向和后向模型检验问题。前-μ演算基于前操作，后-μ演算基于后操作。这两个μ-演算推导出查询逻辑，用布尔空查询扩充定点表达式。使用查询逻辑，我们能够关联和比较符号向后和向前方法。特别是，我们证明了所有ω-正则（线性时间）规范都可以表示为后μ查询，因此可以使用符号前向状态遍历进行检查。另一方面，我们展示了一些简单的分支时间规范不能用这种方式进行检查。
Symbolic model checking, which enables the automatic verification of large systems, proceeds by calculating expressions that represent state sets. Traditionally, symbolic model-checking tools are based on backward state traversal; their basic operation is the function pre, which, given a set of states, returns the set of all predecessor states. This is because specifiers usually employ formalisms with future-time modalities, which are naturally evaluated by iterating applications of pre. It has been shown experimentally that symbolic model checking can perform significantly better if it is based, instead, on forward state traversal; in this case, the basic operation is the function post, which, given a set of states, returns the set of all successor states. This is because forward state traversal can ensure that only parts of the state space that are reachable from an initial state and relevant for the satisfaction or violation of the specification are explored; that is, errors can be detected as soon as possible.In this paper, we investigate which specifications can be checked by symbolic forward state traversal. We formulate the problems of symbolic backward and forward model checking by means of two μ-calculi. The pre-μ calculus is based on the pre operation, and the post-μ calculus is based on the post operation. These two μ-calculi induce query logics, which augment fixpoint expressions with a boolean emptiness query. Using query logics, we are able to relate and compare the symbolic backward and forward approaches. In particular, we prove that all ω-regular (linear-time) specifications can be expressed as post-μ queries, and therefore checked using symbolic forward state traversal. On the other hand, we show that there are simple branching-time specifications that cannot be checked in this way.