1

私はちょうどこの質問を思いつきました。Logic in Computer Science の本に書かれているように、LTL と同等の重要なものの 1 つに 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 による本 Model Checking でこのように定義されていると思います)。

パス 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 の名前をk1andに変更しました):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次に、2 番目の部分が真です。なぜなら、成り立たないiそのようなものが存在する場合、それが成り立つことがわかっているからです。しかし、その場合、は よりも厳密に小さいため、 を選択したことになります。s^i ⊨ not ps^i |= pik1ik1

したがって、式 (1) と (2) はどちらも同等です。

于 2015-06-12T21:33:10.820 に答える