重新开始学数学 • 数理逻辑（5）

我们的目标是写出一个函数，输入一个 CTL 模型和一个 Formula，输出模型中所有能 satisfy 这个 Formula 的状态集合。

fn satisfiable_states(self: &CTLModule, formula: CTLFormula)

根据 CTL 中连接词的定义，我们可以写出：

fn satisfiable_states(self: &CTLModule, formula: CTLFormula) {
    match formula {
        ⊤ => self.S,
        ⊥ => ∅,
        Atomic(atomic) => {s ∈ self.S | atomic is true in state s},
        Not(inner_formula) => self.S - model.sat(inner_formula),
        inner_formula1 ∧ inner_formula2 => model.sat(inner_formula1) ∩ model.sat(inner_formula2),
        inner_formula1 ∨ inner_formula2 => model.sat(inner_formula1) ∪ model.sat(inner_formula2),
        inner_formula1 → inner_formula2 => model.sat(Not(inner_formula1) ∨ inner_formula2),
        // suppose we want to solve EX instead of AX, following ones are similar
        AX(inner_formula) => model.sat(Not(EX(Not(inner_formula)))),
        A[inner_formula1 U inner_formula2] => sat(Not(E[Not(inner_formula2) U (Not(inner_formula1) ∧ Not(inner_formula2))] ∨ EG Not(inner_formula2)))
        EF(inner_formula1) => sat(E[⊤ U inner_formula1])
        EG(inner_formula1) => sat(Not(AF(Not(inner_formula1))))
        AG(inner_formula1) => sat(Not(EF(Not(inner_formula1))))

        EX(inner_formula) => todo!(),
        AF(inner_formula) => todo!(),
        E[inner_formula1 U inner_formula2] => todo!(),
    }
}

Now we've done the trivial cases and "merged" the other cases into three.

然后我们一个个解这三个 case。

EX

能满足 EX(inner_formula) 的状态，也就是“存在一个后继状态满足 inner_formula” 的状态。

只需要先找出所有能满足 inner_formula 的状态，再找出他们所有的前驱状态即可。

EX(inner_formula) => {
    let direct_satisfy = model.sat(inner_formula);
    direct_satisfy
        .map(|satisfying_state| model.predecessors(satisfying_state))
        .union_all()
},

AF

能满足 AF(inner_formula) 的状态，也就是“对于所有从这个点分散出去的 branch，inner_formula 都会在某状态下成立”的状态。

首先能满足 inner_formula 的所有 state 肯定满足上述条件，然后如果某个 state 的前驱的所有后继也都满足条件，那“这个 state 的前驱”也满足条件。

AF(inner_formula) => {
    let direct_satisfy = model.sat(inner_formula);
    let mut current_satisfied = direct_satisfy;
    let mut last_iteration_satisfied = None;
    while last_iteration_satisfied != current_satisfied {
        last_iteration_satisfied = Some(current_satisfied);
        current_satisfied = current_satisfied.union({s ∈ self.S | forall model.successor(s), s is in current_satisfied});
    }
    current_satisfied
}

EU

这个 case 稍微复杂些，E[inner_formula1 U inner_formula2] 的语意是存在某个 path，使得 inner_formula1 至少成立到 inner_formula2 成立为止。

首先由于 U 对 inner_formula2 成立后 inner_formula1 是否继续成立不做要求，所以所有 inner_formula2 成立的 state 都满足条件。

接着，对于所有已知满足条件的状态，如果他的前驱能满足 inner_formula1，那么这个状态也满足条件。

E[inner_formula1 U inner_formula2] => {
    let satisfy_formula1 = model.sat(inner_formula1);
    let satisfy_formula2 = model.sat(inner_formula2);
    let mut current_satisfied = satisfy_formula2;
    let mut last_iteration_satisfied = None;
    while last_iteration_satisfied != current_satisfied {
        last_iteration_satisfied = Some(current_satisfied);
        current_satisfied = current_satisfied.union(model.successor(s).intersect(satisfy_formula1));
    }
}

如此一来我们就完成了这整个算法。