計算木論理のソースを表示

'''計算木論理'''（けいさんきろんり、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の[[well-formed formula|論理式]]である。

<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> - '''A'''ll: <math>\phi</math> は現在状態から分岐する全ての経路で真である。
** '''E''' <math>\phi</math> - '''E'''xists: 現在状態から分岐する経路のうち少なくとも1つの経路で <math>\phi</math> が真である。
* 状態作用素（State Operators）
** '''N''' <math>\phi</math> - '''N'''ext: <math>\phi</math> は次の状態で真である（'''X''' と表記されることもある）。
** '''G''' <math>\phi</math> - '''G'''lobally: <math>\phi</math> はその後の全ての経路で常に真である。
** '''F''' <math>\phi</math> - '''F'''inally: <math>\phi</math> はその後の経路のいずれかの時点で真となる。
** <math>\phi</math> '''U''' <math>\psi</math> - '''U'''ntil: <math>\phi</math> は、ある時点で <math>\psi</math> が真となるまでは真である。これは、将来 <math>\psi</math> が真かどうか検証されることを意味する。
** <math>\phi</math> '''W''' <math>\psi</math> - '''W'''eak 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'''[true'''U'''<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'''[true'''U'''<math>\neg</math><math>\phi</math>]
* '''AF'''<math>\phi</math> == '''A'''[1'''U'''<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>)
<!---
* '''F''' <math>\phi</math> = '''true''' '''U''' <math>\phi</math>
* '''G''' <math>\phi</math> = <math>\neg</math> '''F''' <math>\neg</math><math>\phi</math>
--->

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

: '''AG'''.P
:: 私は今後何があろうともチョコレートが好きだ。
: '''EF'''.P
:: 私がいずれそのうちチョコレートが好きになる日が来る可能性はある。
: '''AF'''.'''EG'''.P
:: ある日絶対に(AF)、私はチョコレートを好きになり、永遠に好きな状態のままとなる。（生涯好き、ではない点に注意。人間の生涯は有限だが、'''G''' は無限を表している）
: '''EG'''.'''AF'''.P
:: 今は私の人生で重大な岐路である。次に起きることによっては(E)、今後ずっと(G)、いつの日か必ず私はチョコレートを好きになる(AF)。しかし、もし悪いことが次に起きると、事態は全く違って、私がチョコレート好きになるかどうかは保証できない。
: '''A'''(P'''U'''Q)
:: 今後、外が暖かくなるまで、毎日私はチョコレートが好きである。しかし一旦外が暖かくなると、もはや私がチョコレートが好きである保証はなくなる。また、たとえ一日であっても、将来外が暖かくなる時が来ると保証される。
: '''E'''(('''EX'''.P)'''U'''('''AG'''.Q))
:: 次のような可能性がある(E)。ある日からずっと外が暖かくなる(AG.Q)。その日までは常に、翌日に私がチョコレートを好きになる何らかのきっかけが存在する(EX.P)。

== 他の論理との関係 ==
計算木論理(CTL)は[[線形時相論理]](LTL)と同様 [[CTL*]][[:en: CTL*|(英語版)]] のサブセットである。CTL と LTL は共通部分もあるが等価ではない。
* '''GF'''.P は LTL にはあるが CTL にはない。
* '''AG'''(P<math>\rightarrow</math>('''EF'''.Q)) は CTL にはあるが LTL にはない。

== 参考文献 ==
* {{cite journal | author=Michael Huth and Mark Ryan | title=Logic in Computer Science(Second Edition) | date=2004年| pages=207 | publisher=Cambridge University Press | id=ISBN 0-521-54310-X}}
* {{cite journal | author=Emerson, E. A. and Halpern, J. Y. | title=Decision procedures and expressiveness in the temporal logic of branching time | journal=Journal of Computer and System Sciences| date=1985年| volume=30 | issue=1 | pages=1-24}}
* {{cite journal | author=Clarke, E. M., Emerson, E. A., and Sistla, A. P. | title=Automatic verification of finite-state concurrent systems using temporal logic specifications | journal=ACM Transactions on Programming Languages and Systems| date=1986年| volume=8 | issue=2 | pages=244-263}}
* {{cite book | author=Emerson, E. A. | date=1990年 | chapter =Temporal and modal logic | editor=J. van Leeuwen (ed.) | title=Handbook of Theoretical Computer Science, vol. B | pages=pp. 955-1072 | publisher=MIT Press | id=ISBN 0-262-22039-3}}

== 関連項目 ==
* [[線形時相論理]]

{{DEFAULTSORT:けいさんきろんり}}
[[Category:理論計算機科学]]
[[Category:論理学]]
[[Category:時相論理]]
[[Category:数学に関する記事]]