通过 SAT 求解进行模型与程序修复

我们考虑以下\emph{模型修复问题}：给定一个有限 Kripke 结构 $M$ 和某个模态或时序逻辑中的规范公式 $\eta$，确定 $M$ 是否包含一个满足 $\eta$ 的子结构 $M'$（具有相同的初始状态）。因此，可以通过删除某些转换来“修复”$M$ 以满足规范 $\eta$。我们将模型修复的一个实例 $(M, \eta)$ 映射为一个布尔公式 $\repfor(M,\eta)$，使得 $(M, \eta)$ 有解当且仅当 $\repfor(M,\eta)$ 是可满足的。此外，一个满足赋值决定了必须从 $M$ 中删除哪些转换以生成 $\eta$ 的模型 $M'$。因此，我们可以使用任何 SAT 求解器来修复 Kripke 结构。此外，使用完备的 SAT 求解器可产生一种完备算法：如果存在修复方案，它总能找到。我们将该方法扩展至修复有限状态共享内存并发程序，求解离散事件监督控制问题 \cite{RW87,RW89}，检查对称解的存在性 \cite{ES93}，并适应关于修复模型中状态和转换存在性的任何布尔约束。最后，我们证明了对于 CTL 以及那些 CTL 可在多项式时间内归约到的具有多项式模型检测算法的逻辑，模型修复是 NP 完全的。此类逻辑的一个显著例子是交替时序逻辑 (ATL)。