1

我只是想出了这个问题。正如在 Logic in Computer Science 一书中所写，LTL 的重要等价之一是：Fp=TUp。T 表示没有约束。

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

4

1 回答 1

0

简短的回答：

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

和一个证明：

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

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

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

（作为删除第一步的s^i路径。）si

我们有（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 重命名为k1andk2以避免混淆）：

    ∃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成立。但在那种情况下，我们会选择ifork1因为iis 严格小于 then k1。

所以公式（1）和（2）是等价的。

于 2015-06-12T21:33:10.820 回答