計算木論理

${\displaystyle \phi$ ::=F|T|p|(\neg \phi )|(\phi \land \phi )|(\phi \lor \phi )|(\phi \rightarrow \phi )|AX\phi |EX\phi |AF\phi |EF\phi |AG\phi |EG\phi |A[\phi U\phi ]|E[\phi U\phi ]}

ここで、p は原子項である。A は「すべての経路について; along All Paths」（必然的に）を表し、E は「少なくとも1つの経路が存在し; along at least there Exists one path」（時には）を表す。例えば、以下はCTLの論理式である。

${\displaystyle EFEGp\rightarrow AFr}$

しかし、以下はCTLの論理式ではない。

${\displaystyle EF(rUq)}$

この文字列の問題点は、U に前置されるのが必ず A か E でなければならないという構文規則を守っていない点である。

CTL は一階述語論理の語彙を構成要素として利用し、それにさらに時相の様相作用素を交えた論理式を生成する。

Summarize Timeline Fact Check

論理作用素は ${\displaystyle \neg ,\lor ,\land ,\rightarrow }$ や ${\displaystyle \leftrightarrow }$ といった一般的なものである。その他にブーリアンの定数 true と false も使用することがある。

時相作用素には以下のものがある:

• 経路作用素（Path Operators）
  • A ${\displaystyle \phi }$ - All: ${\displaystyle \phi }$ は現在状態から分岐する全ての経路で真である。
  • E ${\displaystyle \phi }$ - Exists: 現在状態から分岐する経路のうち少なくとも1つの経路で ${\displaystyle \phi }$ が真である。
• 状態作用素（State Operators）
  • N ${\displaystyle \phi }$ - Next: ${\displaystyle \phi }$ は次の状態で真である（X と表記されることもある）。
  • G ${\displaystyle \phi }$ - Globally: ${\displaystyle \phi }$ はその後の全ての経路で常に真である。
  • F ${\displaystyle \phi }$ - Finally: ${\displaystyle \phi }$ はその後の経路のいずれかの時点で真となる。
  • ${\displaystyle \phi }$ U ${\displaystyle \psi }$ - Until: ${\displaystyle \phi }$ は、ある時点で ${\displaystyle \psi }$ が真となるまでは真である。これは、将来 ${\displaystyle \psi }$ が真かどうか検証されることを意味する。
  • ${\displaystyle \phi }$ W ${\displaystyle \psi }$ - Weak until: ${\displaystyle \phi }$ は、${\displaystyle \psi }$ が真となるまでは真である。U との違いは、将来 ${\displaystyle \psi }$ が真かどうか検証される保証がない点である。"unless"" 作用素とも呼ぶ。

CTL* では、時相作用素は自由に混合できる。CTL では作用素は上記のように2つにグループ分けされ、経路作用素と状態作用素の組み合わせだけが可能である。後述の例を参照されたい。

CTL には作用素の最小セットがある。全てのCTLの論理式は、この最小セットだけを使った論理式に書き換え可能である。これはモデル検査の際に便利である。最小セットの例として {false, ${\displaystyle \lor ,\neg }$, EG, EU, EX} がある。

以下に時相作用素に関する書き換えの例を示す:

• EF${\displaystyle \phi }$ == E[trueU${\displaystyle \phi }$]
• AX${\displaystyle \phi }$ == ${\displaystyle \neg }$EX(${\displaystyle \neg }$${\displaystyle \phi }$)
• AG${\displaystyle \phi }$ == ${\displaystyle \neg }$EF${\displaystyle \neg }$${\displaystyle \phi }$ == ${\displaystyle \neg }$ E[trueU${\displaystyle \neg }$${\displaystyle \phi }$]
• AF${\displaystyle \phi }$ == A[1U${\displaystyle \phi }$] == ${\displaystyle \neg }$EG(${\displaystyle \neg }$${\displaystyle \phi }$)
• A[${\displaystyle \phi }$U${\displaystyle \psi }$] == ${\displaystyle \neg }$(E[${\displaystyle \neg }$${\displaystyle \psi }$U${\displaystyle \neg }$(${\displaystyle \phi }$ ${\displaystyle \lor }$ ${\displaystyle \psi }$)] ${\displaystyle \lor }$ EG ${\displaystyle \neg }$ ${\displaystyle \psi }$)

P の意味が「私はチョコレートが好きだ」であるとし、Q の意味が「外は暖かい」であるとする。

AG.P

私は今後何があろうともチョコレートが好きだ。

EF.P

私がいずれそのうちチョコレートが好きになる日が来る可能性はある。

AF.EG.P

ある日絶対に(AF)、私はチョコレートを好きになり、永遠に好きな状態のままとなる。（生涯好き、ではない点に注意。人間の生涯は有限だが、G は無限を表している）

EG.AF.P

今は私の人生で重大な岐路である。次に起きることによっては(E)、今後ずっと(G)、いつの日か必ず私はチョコレートを好きになる(AF)。しかし、もし悪いことが次に起きると、事態は全く違って、私がチョコレート好きになるかどうかは保証できない。

A(PUQ)

今後、外が暖かくなるまで、毎日私はチョコレートが好きである。しかし一旦外が暖かくなると、もはや私がチョコレートが好きである保証はなくなる。また、たとえ一日であっても、将来外が暖かくなる時が来ると保証される。

E((EX.P)U(AG.Q))

次のような可能性がある(E)。ある日からずっと外が暖かくなる(AG.Q)。その日までは常に、翌日に私がチョコレートを好きになる何らかのきっかけが存在する(EX.P)。