0

私は CTL 演習を行っています。次の式が同等かどうかを確認しようとしています。しかし、私は正しいことをしているかどうかわかりません。

EF (p or q) = EF(p) or EF(q) ? 
AF(p or q) = AF(p) or AF(q) ? 
A(p U ( A(q U r) )) = A(A(p U q) U r) ?

最初の式: 等価

2 番目の式: 等価

3 番目の式: 等価

そうですか？間違っている場合は、クリプキ モデルで考えられる反例の 1 つを教えていただけますか?

前もって感謝します。

4

1 に答える 1

0

ここで定義されている CTL のセマンティクスを使用してみます: CTL についてのウィキペディア。

(I) 証明のためEF (p or q) = EF(p) or EF(q):

(M, s1) |= EF (p or q)*

<=> (Def. of EF)

There is s1->s2->... such that there is an i >= 1 such that (M, s_i) |= (p or q)

<=> (Def. of or)

There is s1->s2->... such that is an i >= 1 such that ((M, s_i) |= p OR ((M, s_i) |= q)

<=> (Equivalence rules for predicate logic)


(There is s1->s2->... such that is an i >= 1 such that ((M, s_i) |= p)
 OR 
(There is s1->s2->... such that is an i >= 1 such that ((M, s_i) |= q)

<=> (Def. of EF)

EF(p) or EF(q)

したがって、同等性は有効です。

(Ⅱ)

AF(p or q) = AF(p) or AF(q)

3 つの状態 S0、S1、S2 を持つ Kripke 構造を想定し、S0 を初期状態とします。S0 ではどちらもp nor q成り立たず、S1 ではp成り立ち、S2 ではq成り立ちません。

遷移は次のとおりです。

S0 -> S1
S0 -> S2
S1 -> S1
S2 -> S2

S1 は SCC を形成し、S2 は SCC を形成します。(p または q) は S0 を除くすべての状態で成り立ち、最終的にすべてのシーケンスが S1 または S2 に到達するため、この Kripke 構造では AF(p または q) が成り立ちます。AF(p)またはAF(q)はどうですか? S0 S2 S2 S2 ... という p が現れないシーケンスがあるため、AF(p) は成立しません。AF(q) は成立しません。なぜなら、シーケンス S0 S1 S1 S1 ... で q が現れないからです。

(III) の場合: 上で使用した手法を使用して、証明を楽しんでください :)

于 2016-01-24T14:15:18.503 に答える