CTL与一阶时态逻辑推理方法研究及实验分析

### CTL与一阶时态逻辑推理方法研究及实验分析 #### CTL证明器的实现与实验 在计算树逻辑（CTL）的研究中，我们实现了从CTL到SNFg CTL的转换以及R≻,S CTL演算，具体是在证明器CTL - RP中完成的。R≻,S CTL的实现借鉴了实现命题线性时态逻辑（PLTL）归结演算的方法。具体操作步骤如下： 1. **转换为一阶子句**：将除A - 和E - 有时子句之外的所有SNFg CTL子句转换为一阶子句。 2. **模拟步骤归结**：利用一阶有序归结与选择来模拟步骤归结。 3. **实现终态归结规则**：实现了E - 循环搜索算法来处理终态归结规则，并将终态归结规则应用的结果以一阶子句的形式计算出来。 4. **借助已有工具**：为实现一阶有序归结与选择，复用了一阶定理证明器SPASS 3.0的实现。 5. **消除冗余**：采用SPASS的一些技术来消除冗余，包括重言式删除、前向包含、后向包含以及匹配替换归结的改进版本。 除了CTL - RP，已知的CTL定理证明器还有Tableau Workbench（TWB）中的CTL模块。TWB是构建任意命题逻辑自动定理证明器的通用框架，它为多种逻辑提供了预定义的证明器，在CTL方面，它实现了单遍表推演演算，其CTL决策过程的复杂度为双指数时间（double - EXPTIME），高于CTL - RP的指数时间（EXPTIME）复杂度，且TWB的主要目标并非追求效率。 为了评估CTL决策过程的性能，我们创建了三组基准公式，用于比较CTL - RP版本00.09和TWB版本3.4。实验在配备Intel Core 2 E6400 CPU @ 2.13 GHz和3GB主内存的Linux PC上进行，使用Fedora 9操作系统。 - **第一组基准公式（CTL - BF1）**：由八个著名的时态公式等价式组成。两个系统都能在不到0.1秒的时间内证明每个公式，但TWB在其中两个公式上明显更快，具体性能数据如下表所示： | CTL等价式 | CTL - RP | TWB | | --- | --- | --- | | A2p ≡¬E3¬p | 0.008s | 0.005s | | E2p ≡¬A3¬p | 0.008s | 0.004s | | E(p ∨q) ≡Ep ∨Eq | 0.005s | 0.005s | | Ap ≡¬E¬p | 0.004s | 0.006s | | E(p U q) ≡q ∨(p ∧EE(p U q)) | 0.049s | 0.005s | | A(p U q) ≡q ∨(p ∧AA(p U q)) | 0.068s | 0.005s | | E3p ≡E(true U p) | 0.010s | 0.008s | | A3p ≡A(true U p) | 0.010s | 0.008s | - **第二组基准公式（CTL - BF2）**：通过随机生成由状态转换系统规范和待验证系统属性组成的公式得到。具体生成方式如下： - **状态规范**：是文字li（1 ≤ i ≤ 4）的合取，每个li属于{ai, ¬ai}。 - **转换规范**：是形式为A2(s ⇒A(∧n i = 1 si))或A2(s ⇒E(∧n i = 1 si))的CTL公式，其中n是1到3之间的随机数，s和每个si（1 ≤ i ≤ n）是随机生成的状态规范。 - **属性规范**：是形式为∗(∧n i = 1 si)（∗是{A, E, A2, E2, A3, E3