計算木論理
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)。
φ ::= F | T | p | ( ¬ φ ) | ( φ ∧ φ ) | ( φ ∨ φ ) | ( φ → φ ) | A X φ | E X φ | A F φ | E F φ | A G φ | E G φ | A [ φ U φ ] | E [ φ U φ ] {\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の論理式である。
E F E G p → A F r {\displaystyle EFEGp\rightarrow AFr}
しかし、以下はCTLの論理式ではない。
E F ( r U q ) {\displaystyle EF(rUq)}
この文字列の問題点は、U に前置されるのが必ず A か E でなければならないという構文規則を守っていない点である。
CTL は一階述語論理の語彙を構成要素として利用し、それにさらに時相の様相作用素を交えた論理式を生成する。