无限转移系统同步积的模型检测

基于模型检测范式的形式化验证必须处理两个方面：系统模型是结构化的，通常表现为组件的积；规范逻辑必须具有足够的表达能力以允许形式化可达性属性。本文研究了在这些前提下针对无限转移系统所能取得的成果。作为模型，我们考虑具有不同同步约束的无限转移系统的积。我们引入了有限同步转移系统，即仅包含有限多个（参数化）同步转移的积系统，并表明积系统的 FO(R)（由可达性谓词扩展的一阶逻辑）的可判定性可归约为其组件的 FO(R) 可判定性。该结果在以下意义上是最优的：(1) 如果允许半有限同步，即仅在一个组件中有无限多个转移被同步，则积系统的 FO(R) 理论通常是不可判定的。(2) 我们无法扩展所考虑逻辑的表达能力。即使是对一阶逻辑进行带有传递闭包的弱扩展（其中我们将传递闭包算子限制为 arity 一且嵌套深度为二），对于异步（因而也是有限同步）积（例如无限网格）而言也是不可判定的。