Model checking synchronized products of infinite transition systems
Model checking synchronized products of infinite transition systems
复制标题
模型检查无限过渡系统的同步乘积
DOI：
10.2168/lmcs-3(4:5)2007
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
W. Thomas
中科院分区：
文献类型：
--
作者：
Stefan Wöhrle;W. Thomas
使用模型检查范式的形式验证必须处理两个方面。系统模型是结构化的，通常作为组件的产品，并且规范逻辑必须具有足够的表达能力，以允许可达性属性的形式化。本文研究了在这些前提下无限转移系统可以实现的目标。作为模型，我们考虑具有不同同步约束的无限转移系统的产物。我们引入有限同步转移系统，即仅包含有限多个同步转移的乘积系统，并表明乘积系统的由可达性谓词扩展的一阶逻辑 FO(R) 的可判定性可以以类似 Feferman-Vaught 的方式简化为组件 FO(R) 的可判定性。该结果在以下意义上是最佳的。 (1) 如果我们允许半有限同步，即仅在一个组件中同步无限多个转换，则乘积系统的 FO(R) 理论通常是不可判定的。 (2) 我们无法扩展所考虑的逻辑的表达能力。具有传递闭包的一阶逻辑的弱扩展（我们将传递闭包运算符限制为元数一和嵌套深度二）对于异步（因此有限同步）产品（即无限网格）来说是不可判定的。
Formal verification using the model-checking paradigm has to deal with two aspects. The systems models are structured, often as products of components, and the specification logic has to be expressive enough to allow the formalization of reachability properties. The present paper is a study on what can be achieved for infinite transition systems under these premises. As models, we consider products of infinite transition systems with different synchronization constraints. We introduce finitely synchronized transition systems, i.e. product systems which contain only finitely many synchronized transitions, and show that the decidability of FO(R), first-order logic extended by reachability predicates, of the product system can be reduced to the decidability of FO(R) of the components in a Feferman-Vaught like style. This result is optimal in the following sense. (1) If we allow semifinite synchronization, i.e. just in one component infinitely many transitions are synchronized, the FO(R)-theory of the product system is in general undecidable. (2) We cannot extend the expressive power of the logic under consideration. Already a weak extension of first-order logic with transitive closure, where we restrict the transitive closure operators to arity one and nesting depth two, is undecidable for an asynchronous (and hence finitely synchronized) product, namely for the infinite grid.