時相論理

出典: フリー百科事典『ウィキペディア（Wikipedia）』

時相論理（Temporal Logic）とは、時間との関連で問題を理解し表現するための規則と表記法の体系である。1960年代に Arthur Prior が提唱した様相論理学に基づいた時相論理を特に時制論理（Tense Logic）と呼ぶことがある。その後、そこから発展し、アミール・プヌーリら計算機科学者や論理学者が研究を進めた。

[編集] 概要

時相論理を最初に研究したのはアリストテレスであった。彼の記したものには一階述語/時相/様相/二値/論理の原始的な記述が多い。存在記号や全称記号を使った論理は一種の一階述語論理である。時間を状態変化として観測する論理は時相論理であり、二値の真理値を使用する論理は二値論理と言える。

「私は腹ペコだ」という文を考えてみよう。この文の意味は時間経過に関わらず一定であるが、その真偽は時間経過によって変化する。あるときは真だし、またあるときは偽である。しかし、同時に真でもあり偽でもあるということはありえない。時相論理では、時と共に真理値の変化する文を扱う。非時相論理では、時間経過によって真理値が変化しない文しか扱えない。

時相論理では、「私はいつも腹ペコだ」、「私はそのうち腹ペコになる」、「私は何かを食べるまで腹ペコだろう」といった文を表現できる。

時相論理はシステムのハードウェアやソフトウェアの要求仕様を記述する方法として形式的検証で利用される。例えば、「要求が発生したら常にリソースへのアクセスがそのうちに承認される。ただし、決して2つの要求を同時に承認してはならない」といった文章は時相論理で表せるのである。

時相論理は常に時系列について判断する能力を有する。線形時間論理（Linear Time Logic）と呼ばれるものはこの種の推論に限定されている。分岐論理（Branching Logic）は複数の時系列を判断できる。これは予測不能な挙動を示す環境を前提とする。さらに言えば、分岐論理では「私が永遠に腹ペコのままでいる可能性がある」といった文が表現可能である。他にも「私がもう腹ペコではなくなる可能性がある」という文も表現可能である。「私」が食べ物にありつけるかどうか不明ならば、これらの文はどちらも真である。

形式的検証では、線形時相論理（アミール・プヌーリと Zohar Manna による線形時間論理の一種）と計算木論理（Edmund Clarke と E. Allen Emerson による分岐時間論理の一種）が競っている。後者のほうが分岐を扱えるぶんだけ前者よりも効果的であると指摘されることがある。Emerson と Lei は、いかなる線形論理も複雑性を変えずに分岐論理に拡張可能であることを示した。

[編集] 時相作用素

時相論理では2種類の作用素を使用する。論理作用素と様相作用素である[1]。論理作用素は一般的な真理関数作用素である( $\neg,\or,\and,\rightarrow$ )。線形時相論理や計算木論理で使用される様相作用素を以下に示す。

文字表記	記号表記	定義	説明	ダイアグラム
二項演算
$φ$ U $ψ$	$\phi ~\mathcal{U}~ \psi$	$\begin{matrix}(B\mathcal{U}C)(\phi)= \\ (\exists i:C(\phi_i))\land(\forall j<i:B(\phi_j))\end{matrix}$	Until: $ψ$ は現在あるいは未来の位置で有効で、 $φ$ はそれ以前の位置まで有効でなければならない。その位置で $φ$ は保持する必要はなくなる。
$φ$ R $ψ$	$\phi ~\mathcal{R}~ \psi$	$\begin{matrix}(B\mathcal{R}C)(\phi)= \\ (\forall i:C(\phi_i))\lor(\exists j<i:B(\phi_j))\end{matrix}$	Release: $φ$ が真である最初の位置まで $ψ$ が真であるならば（またはそのような位置がないなら永久に）、 $φ$ は $ψ$ をリリースする。
単項演算
X $φ$	$\circ \phi$	$\mathcal{N}B(\phi_i)=B(\phi_{i+1})$	Next: $φ$ は次の状態で有効でなければならない。（X は同義語的に使われる）
F $φ$	$\Diamond \phi$	$\mathcal{F}B(\phi)=(true\mathcal{U}B)(\phi)$	Finally: $φ$ は結局、有効となる必要がある。（将来のいずれかの時点で）
G $φ$	$\Box \phi$	$\mathcal{G}B(\phi)=\neg\mathcal{F}\neg B(\phi)$	Globally: $φ$ はその後ずっと有効である必要がある。
A $φ$		$\begin{matrix}(\mathcal{A}B)(\psi)= \\ (\forall \phi:\phi_0=\psi\to B(\phi))\end{matrix}$	All: $φ$ は現在状態から生ずる全てのパス上で有効である必要がある。
E $φ$		$\begin{matrix}(\mathcal{E}B)(\psi)= \\ (\exists \phi:\phi_0=\psi\land B(\phi))\end{matrix}$	Exists: 現在状態から生じるパスの少なくとも1つで $φ$ が有効なものがある。

他の表現:

作用素 R は V で表記されることがある。
作用素 W は weak until を意味する。 $f W g$ は $f U g \or G f$ と等価である。

B( $φ$ ) が整論理式(wff)であれば、単項作用素は全て整論理式である。B( $φ$ ) と C( $φ$ ) が整論理式であれば、二項作用素は全て整論理式である。

論理体系によっては一部の作用素は表現できない。例えば、Temporal Logic of Actions では N 作用素は表現できない。

[編集] 時相論理からの派生

計算木論理 (CTL)
線形時相論理 (LTL)
インターバル時相論理 (ITL)
μ計算

[編集] 参考文献

Venema, Yde, 2001, "Temporal Logic," in Goble, Lou, ed., The Blackwell Guide to Philosophical Logic. Blackwell.
E. A. Emerson and C. Lei, modalities for model checking: branching time logic strikes back, in Science of Computer Programming 8, p 275-306, 1987.
E.A. Emerson, Temporal and modal logic, Handbook of Theoretical Computer Science, Chapter 16, the MIT Press, 1990