計算木論理

計算木論理（けいさんきろんり、Computational Tree Logic、CTL）は、分岐時相論理の一種である。その時間モデルでは未来は決定されておらず木構造のように分岐している。未来の複数の経路のうちの1つが実際に現実の経路となる。

文法

[math]\phi::=F|T|p|(\neg\phi)|(\phi\and\phi)|(\phi\or\phi)| (\phi\rightarrow\phi)|AX\phi|EX\phi|AF\phi|EF\phi|AG\phi|EG\phi| A[\phi U \phi]|E[\phi U \phi][/math]

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

[math]EF EG p \rightarrow AF r [/math]

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

[math]EF (r U q) [/math]

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

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

作用素

論理作用素

論理作用素は [math]\neg,\or,\and,\rightarrow[/math] や [math]\leftrightarrow[/math] といった一般的なものである。その他にブーリアンの定数 true と false も使用することがある。

時相作用素

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

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

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

作用素の最小セット

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

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

• EF[math]\phi[/math] == E[trueU[math]\phi[/math]]
• AX[math]\phi[/math] == [math]\neg[/math]EX([math]\neg[/math][math]\phi[/math])
• AG[math]\phi[/math] == [math]\neg[/math]EF[math]\neg[/math][math]\phi[/math] == [math]\neg[/math] E[trueU[math]\neg[/math][math]\phi[/math]]
• AF[math]\phi[/math] == A[1U[math]\phi[/math]] == [math]\neg[/math]EG([math]\neg[/math][math]\phi[/math])
• A[[math]\phi[/math]U[math]\psi[/math]] == [math]\neg[/math](E[[math]\neg[/math][math]\psi[/math]U[math]\neg[/math]([math]\phi[/math] [math]\or[/math] [math]\psi[/math])] [math]\or[/math] EG [math]\neg[/math] [math]\psi[/math])

例

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)。

他の論理との関係

計算木論理(CTL)は線形時相論理(LTL)と同様 CTL* のサブセットである。CTL と LTL は共通部分もあるが等価ではない。

• GF.P は LTL にはあるが CTL にはない。
• AG(P[math]\rightarrow[/math](EF.Q)) は CTL にはあるが LTL にはない。

関連項目

• 線形時相論理

参考文献

• Michael Huth and Mark Ryan (2004年). Logic in Computer Science(Second Edition). Cambridge University Press. pp. 207. ISBN 0-521-54310-X. 
• Emerson, E. A. and Halpern, J. Y. (1985年). “Decision procedures and expressiveness in the temporal logic of branching time”. Journal of Computer and System Sciences 30 (1): 1-24. 
• Clarke, E. M., Emerson, E. A., and Sistla, A. P. (1986年). “Automatic verification of finite-state concurrent systems using temporal logic specifications”. ACM Transactions on Programming Languages and Systems 8 (2): 244-263. 
• Emerson, E. A. (1990年). “Temporal and modal logic”, in J. van Leeuwen (ed.): Handbook of Theoretical Computer Science, vol. B. MIT Press, pp. 955-1072. ISBN 0-262-22039-3.