LTL 关于Fp=TUp，重写F 真的有必要T 吗？

Question

我刚想出这个问题。正如计算机科学逻辑一书中所写，LTL 的重要等价物之一是： Fp=TUp。 T 表示没有限制。

但是，如果我将 T 替换为（而不是 p）呢？ Fp=(not p)Up 成立吗？因为在这种情况下，我实际上在公式中加入了一些约束（不是 p），但同时可能没有状态可以同时满足（不是 p）和 p。我尝试使用不同的 LTL 公式作为 p，只要 p 是可满足的，那么对于带有 p 的每条路径，它也必须满足 Fp 和（不是 p）Up。这是否意味着我可以用这种方式重写 F 或者有一些反例？

Answer 1

简答：

是的，两个公式是等价的，您也可以用 (¬p)Up.

重写 Fp

和证明：

我们可以通过查看 pUq 的定义来调查问题（我认为它在 Clarke、Grumberg、Peled 的《模型检查》一书中是这样定义的）。

A路径s是公式的模型（写成s ⊨ pUq）：

s ⊨ pUq <=>   ∃k: s^k ⊨ q
            ∧ ∀i: 0<=i<k => s^i ⊨ q

（s^i 是删除前 i 个步骤的路径 s。）

我们有 (1) 个：

s ⊨ (¬p)Up <=>   ∃k: s^k ⊨ p
               ∧ ∀i: 0<=i<k => s^i ⊨ ¬p

和 (2):

s ⊨ TUp <=>   ∃k: s^k ⊨ p
            ∧ ∀i: 0<=i<k => s^i ⊨ true
        <=>   ∃k: s^k ⊨ p

我们要显示 (1) <=> (2)（我将 ks 重命名为 k1 和 k2 以避免混淆）：

    ∃k1: s^k1 ⊨ p
  ∧ ∀i: 0<=i<k1 => s^i ⊨ ¬p
<=>
    ∃k2: s^k2 ⊨ p

方向 (1) => (2) 是微不足道的。

对于 (2) => (1) 我们必须证明

 ∃k2: s^k2 ⊨ p

关注

 ∃k1: s^k1 ⊨ p ∧ ∀i: 0<=i<k1 => s^i ⊨ ¬p

我们知道 k1 存在一个值（即 k2）使得 s^k1 ⊨ p 成立。但是第二部分呢？我们现在可以只使用 k1 满足 s^i ⊨ p 的最小值。那么第二部分为真，因为如果存在 i 使得 s^i ⊨ not p 不成立，我们知道 s^i |= p 成立。但在那种情况下，我们会为 k1 选择 i，因为 i 严格小于 k1。

所以公式(1)和(2)是等价的

LTL 关于Fp=TUp，重写F 真的有必要T 吗？

LTL about Fp=TUp, is T really necessary in rewriting F?

logic

model-checking