次の CTL 式は同等ではないと言われています。しかし、一方が真で他方が真でないモデルを見つけることができません。CTL は計算時相論理です。
フォーミュラ 1: AF p OR AF q
フォーミュラ 2: AF( p OR q )
1 つ目は、begin 状態から始まるすべてのパスには、p が保持される未来がある、または begin 状態から始まるすべてのパスには、q が保持される未来があるということです。
2 番目: 開始状態から始まるすべてのパスには、p OR q が成立する未来があります。
モデルは少しトリッキーです。まず、 AF(p OR q)はAF p OR AF qを意味することに注意してください。したがって、 AF (p OR q)が true であるが、AF p OR AF qが falseであるモデルを探しています。
M. Huth と M. Ryan による Logic in Computer Science の教科書 ( http://www.cs.bham.ac.uk/research/projects/lics/を参照) で説明されている Kripke モデル表記法に精通していることを前提としています。
M = (S, R, L) を、可能な状態の集合として S = {s0, s1, s2} を持つモデル、R = {(s0,s1), (s0,s2), (s1,s1) とする, (s1,s2), (s2,s2)} であり、L は次のように定義されるラベル付け関数です: L(s0) = {} (空集合)、L(s1) = {p}、およびL(s2) = {q}。
開始状態が s0 であるとします。AF (p OR q)が s0 で成り立つことは明らかです。ただし、s0ではAF p OR AF qは成立しません。これを証明するには、s0 が AF p *を満たさず、 * s0 が AF qを満たさないことを示さなければなりません。
パス s0 -> s2 -> s2 -> s2 -> ... を選択できるため、AF pは s0 で満たされていません。
同様に、パス s0 -> s1 -> s1 -> s1 -> ... を選択できるため、 AF qは s1 で満たされません。