一种改进的CTL子句消解演算

# 一种改进的CTL子句消解演算 ## 1. CTL公式可满足性与转换规则 ### 1.1 CTL公式可满足性 CTL（计算树逻辑）公式 $\phi$ 在模型结构 $M = \langle S, R, L, [ ], s_0 \rangle$ 中是可满足的，当且仅当 $M, s_0 \vDash \phi$。若存在一个模型结构 $M$ 使得 $\phi$ 在其中被满足，则称 $\phi$ 是可满足的。 ### 1.2 CTL公式转换规则 我们定义了一组转换规则，可将任意CTL公式转换为等价可满足的SNFg CTL子句集。转换规则与某些已有规则类似，但进行了修改以支持全局子句。主要使用以下技术： - 向E路径量词引入新索引； - 用新原子命题重命名复杂子公式，并将新原子命题的真值与被重命名子公式的真值关联起来； - 利用其他运算符的语义定义，移除SNFg CTL子句中不允许出现的时态运算符组合。 以下是两个转换规则的示例： - $A2(q \Rightarrow E\square\phi)$ 转换为 $A2(q \Rightarrow E\langle ind \rangle\square\phi)$，为 $E\square$ 运算符分配一个索引。 - $A2(q_1 \Rightarrow E\langle ind \rangle(q_2 U q_3))$ 转换为 $A2(q_1 \Rightarrow q_3 \vee (q_2 \wedge p))$、$A2(p \Rightarrow E\langle ind \rangle\square(q_3 \vee (q_2 \wedge p)))$ 和 $A2(q_1 \Rightarrow E\langle ind \rangle\Diamond q_3)$，消除 $E\langle ind \rangle U$ 运算符的出现。不过，前两个公式还不是SNFg CTL形式，需要进一步转换。 ### 1.3 范式定理 每个CTL公式 $\phi$ 都可以转换为一个等价可满足的SNFg CTL子句集 $T$，且问题规模最多线性增加。 ## 2. 子句消解演算 $R_{\succ,S}^{CTL}$ ### 2.1 演算组成 $R_{\succ,S}^{CTL}$ 消解演算由两种消解规则（步消解规则SRES1 - SRES8和终态消解规则ERES1和ERES2）以及两个重写规则（RW1和RW2）组成。 ### 2.2 步消解规则 步消解规则SRES1 - SRES8如下： |规则|前提1|前提2|结论| |----|----|----|----| |SRES1|$P \Rightarrow A\square(C \vee l)$|$Q \Rightarrow A\square(D \vee \neg l)$|$P \wedge Q \Rightarrow A\square(C \vee D)$| |SRES2|$P \Rightarrow E\langle ind \rangle\square(C \vee l)$|$Q \Rightarrow A\square(D \vee \neg l)$|$P \wedge Q \Rightarrow E\langle ind \rangle\square(C \vee D)$| |SRES3|$P \Rightarrow E\langle ind \rangle\square(C \vee l)$|$Q \Rightarrow E\langle ind \rangle\square(D \vee \neg l)$|$P \wedge Q \Rightarrow E\langle ind \rangle\square(C \vee D)$| |SRES4|$start \Rightarrow C \vee l$|$start \Rightarrow D \vee \neg l$|$start \Rightarrow C \vee D$| |SRES5|$true \Rightarrow C \vee l$|$start \Rightarrow D \vee \neg l$|$start \Rightarrow C \vee D$| |SRES6|$true \Rightarrow C \vee l$|$Q \Rightarrow A\square(D \vee \neg l)$|$Q \Rightarrow A\square(C \vee D)$| |SRES7|$true \Rightarrow C \vee l$|$Q \Rightarrow E\langle ind \rangle\square(D \vee \neg l)$|$Q \Rightarrow E\langle ind \rangle\square(C \vee D)$| |SRES8|$true \Rightarrow C \vee l$|$true \Rightarrow D \vee \neg l$|$true \Rightarrow C \vee D$| 步消解规则仅在满足以下两个条件之一时适用： - (C1) 若 $l$ 为正文字，则： - $l$ 必须相对于 $C$ 严格最大，且 $C \vee l$ 中没有文字被选择； - $\neg l$ 必须在 $D \vee \neg l$ 中被选择，或者 $D \vee \neg l$ 中没有文字被选择且 $\neg l$ 相对于 $D$ 最大。 - (C2) 若 $l$ 为负文字，则： - $l$ 必须在 $C \vee l$ 中被选择，或者 $C \vee l$ 中没有文字被选择且 $l$ 相对于 $C$ 最大； - $\neg l$ 必须相对于 $D$ 严格最大，且 $D \vee \neg l$ 中没有文字被选择。 如果 $C \vee l$ 中的 $l$ 和 $D \vee \neg l$ 中的 $\neg l$ 满足条件 (C1) 或条件 (C2)，则称 $l$ 在 $C \vee l$ 中是合格的，$\neg l$ 在 $D \vee \neg l$ 中是合格的。 ### 2.3 重写规则 重写规则RW1和RW2定义如下： - RW1: $\bigwedge_{i=1}^{n} m_i \Rightarrow A\square false \rightarrow true \Rightarrow \bigvee_{i=1}^{n} \neg m_i$ - RW2: $\bigwedge_{i=1}^{n} m_i \Rightarrow E\langle ind \rangle\square false \rightarrow true \Rightarrow \bigvee_{i=1}^{n} \neg m_i$ 其中 $n \geq 1$，且每个 $m_i$（$1 \leq i \leq n$）是一个文字。 ### 2.4 终态消解规则 #### 2.4.1 ERES1规则 终态消解规则ERES1的直觉是，将终态 $A\Diamond\neg l$（表示 $\Diamond\neg l$ 在所有路径上为真）与一组SNFg CTL子句进行消解。如果这些子句的左部合取式被满足，那么它们共同意味着 $\square l$ 在（至少）一条路径上成立。 $ERES1$: 前提1: $P^{\dagger} \Rightarrow E\square E\square l$ 前提2: $Q \Rightarrow A\Diamond\neg l$ 结论: $Q \Rightarrow A(\neg(P^{\dagger}) W \neg l)$ 其中，$P^{\dagger} \Rightarrow E\square E\square l$ 表示一组SNFg CTL子句 $\Lambda_{E2}$，对于每个 $i$（$1 \leq i \leq n$），有 $(\bigwedge_{j=1}^{m_i} C_{i}^{j}) \Rightarrow l$ 和 $(\bigwedge_{j=1}^{m_i} C_{i}^{j}) \Rightarrow (\bigwedge_{i=1}^{n} \bigwedge_{j=1}^{m_i} P_{i}^{j})$ 是可证明的，且 $P^{\dagger} = \bigwedge_{i=1}^{n} \bigwedge_{j=1}^{m_i} P_{i}^{j}$。 为了将ERES1的结论表示为范式，我们使用一个与终态 $A\Diamond\neg l