時相論理

時相論理（Temporal Logic）とは、時間との関連で問題を理解し表現するための規則と表記法の体系である。時相論理では、「私はいつも腹ペコだ」、「私はそのうち腹ペコになる」、「私は何かを食べるまで腹ペコだろう」といった文を表現できる。1950年代末にテンプレート:仮リンクが提唱した様相論理に基づいた時相論理を特に時制論理（Tense Logic）と呼ぶことがある。テンプレート:仮リンクが重要な業績を残した。その後、そこから発展し、アミール・プヌーリら計算機科学者や論理学者が研究を進めた。

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

概要

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

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

歴史

アリストテレスは主に三段論法を研究したが、現代の時相論理のような研究もしており、一階時相二値論理のような形式を部分的に検討したことがある。特に不確定な未来の事象を扱う際、アリストテレスは二値の意味論を適用できないと考え、例えば「明日、海戦が勃発するだろう」といった文の真偽を現時点で決定できないとしたテンプレート:Sfn。

その後数千年間、ほとんど発展は見られなかった。19世紀、チャールズ・サンダース・パースは次のように記している。 テンプレート:Cquote

テンプレート:仮リンクは自由意志や予定説といった哲学的問題を検討した。彼の妻によれば、彼が最初に時相論理を定式化したのは1953年のことだという。1955年から56年にかけてオックスフォード大学でそれについて講義をし、1957年には Time and Modality を出版。その中で2つの時相接続子（テンプレート:仮リンク）F（「未来のいずれかの時点で」の意）とP（「過去のいずれかの時点で」の意）を備えた命題様相論理を説明している。この先駆的取り組みで、プライアーは時間を線型なものとみなしている。しかし1958年、ソール・クリプキはプライアーへの手紙で、その仮定は不当だと指摘した。計算機科学での同様な考え方を予示しつつ、プライアーは熟慮の上それを採用し2つの分岐時間の理論を考案、"Ockhamist" と "Peircean" と名付けたテンプレート:Sfnテンプレート:要説明。1958年から1965年にかけて、プライアーは Charles Leonard Hamblin と共同で時相論理について研究した。1967年、時相論理に関する研究の集大成として Past, Present, and Future を出版。その2年後に亡くなった。

テンプレート:仮リンクは1968年の博士論文で二値の時相作用素 Since と Until を導入し、その論文で時相論理と一階述語論理を関連付ける重要な考察も行い、それが「カンプの定理」と呼ばれるようになったテンプレート:Sfn。

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

時相作用素

時相論理では2種類の作用素を使用する。論理作用素とテンプレート:仮リンクである[1]。論理作用素は一般的な真理関数作用素である($\mathrm{\neg },\vee ,\wedge ,\to$)。線形時相論理や計算木論理で使用される様相作用素を以下に示す。

文字表記	記号表記	定義	説明	ダイアグラム
二項演算
$\varphi$ U $\psi$	$\varphi 𝒰\psi$	$\begin{array}{c}(B𝒰C)(\varphi )=\\ (\mathrm{\exists }i:C({\varphi }_i)\wedge (\mathrm{\forall }j<i:B({\varphi }_j)))\end{array}$	Until: $\psi$ は現在あるいは未来の位置で有効で、$\varphi$ はそれ以前の位置まで有効でなければならない。その位置で $\varphi$ は保持する必要はなくなる。	<timeline> ImageSize = width:240 height:94 PlotArea = left:30 bottom:30 top:0 right:20 DateFormat = x.y Period = from:0 till:6 TimeAxis = orientation:horizontal AlignBars = justify ScaleMajor = gridcolor:black increment:1 start:0 ScaleMinor = gridcolor:black increment:1 start:0 PlotData= bar:p color:red width:10 align:left fontsize:S from:1 till:3 bar:q color:red width:10 align:left fontsize:S from:3 till:5 bar:pUq color:red width:10 align:left fontsize:S from:1 till:5 </timeline>
$\varphi$ R $\psi$	$\varphi ℛ\psi$	$\begin{array}{c}(BℛC)(\varphi )=\\ (\mathrm{\forall }i:C({\varphi }_i)\vee (\mathrm{\exists }j<i:B({\varphi }_j)))\end{array}$	Release: $\varphi$ が真である最初の位置まで $\psi$ が真であるならば（またはそのような位置がないなら永久に）、$\varphi$ は $\psi$ をリリースする。	<timeline> ImageSize = width:240 height:100 PlotArea = left:30 bottom:30 top:0 right:20 DateFormat = x.y Period = from:0 till:6 TimeAxis = orientation:horizontal AlignBars = justify ScaleMajor = gridcolor:black increment:1 start:0 ScaleMinor = gridcolor:black increment:1 start:0 PlotData= bar:p color:red width:10 align:left fontsize:S from:2 till:4 bar:q color:red width:10 align:left fontsize:S from:1 till:3 from:5 till:6 bar:pRq color:red width:10 align:left fontsize:S from:1 till:3 from:5 till:6 </timeline>
単項演算
N $\varphi$	$\circ \varphi$	$𝒩B({\varphi }_i)=B({\varphi }_{i+1})$	Next: $\varphi$ は次の状態で有効でなければならない。（X は同義語的に使われる）	<timeline> ImageSize = width:240 height:60 PlotArea = left:30 bottom:30 top:0 right:20 DateFormat = x.y Period = from:0 till:6 TimeAxis = orientation:horizontal AlignBars = justify ScaleMajor = gridcolor:black increment:1 start:0 ScaleMinor = gridcolor:black increment:1 start:0 PlotData= bar:p color:red width:10 align:left fontsize:S from:2 till:3 from:5 till:6 bar:Np color:red width:10 align:left fontsize:S from:1 till:2 from:4 till:5 </timeline>
F $\varphi$	$◊\varphi$	$ℱB(\varphi )=(true𝒰B)(\varphi )$	Finally: $\varphi$ は結局、有効となる必要がある。（将来のいずれかの時点で）	<timeline> ImageSize = width:240 height:60 PlotArea = left:30 bottom:30 top:0 right:20 DateFormat = x.y Period = from:0 till:6 TimeAxis = orientation:horizontal AlignBars = justify ScaleMajor = gridcolor:black increment:1 start:0 ScaleMinor = gridcolor:black increment:1 start:0 PlotData= bar:p color:red width:10 align:left fontsize:S from:2 till:3 from:4 till:5 bar:Fp color:red width:10 align:left fontsize:S from:0 till:5 </timeline>
G $\varphi$	$◻\varphi$	$𝒢B(\varphi )=\mathrm{\neg }ℱ\mathrm{\neg }B(\varphi )$	Globally: $\varphi$ はその後ずっと有効である必要がある。	<timeline> ImageSize = width:240 height:60 PlotArea = left:30 bottom:30 top:0 right:20 DateFormat = x.y Period = from:0 till:6 TimeAxis = orientation:horizontal AlignBars = justify ScaleMajor = gridcolor:black increment:1 start:0 ScaleMinor = gridcolor:black increment:1 start:0 PlotData= bar:p color:red width:10 align:left fontsize:S from:1 till:3 from:4 till:6 bar:Gp color:red width:10 align:left fontsize:S from:4 till:6 </timeline>
A $\varphi$	$\mathrm{\forall }\varphi$	$\begin{array}{c}(𝒜B)(\psi )=\\ (\mathrm{\forall }\varphi :{\varphi }_0=\psi \to B(\varphi ))\end{array}$	All: $\varphi$ は現在状態から生ずる全てのパス上で有効である必要がある。
E $\varphi$	$\mathrm{\exists }\varphi$	$\begin{array}{c}(ℰB)(\psi )=\\ (\mathrm{\exists }\varphi :{\varphi }_0=\psi \wedge B(\varphi ))\end{array}$	Exists: 現在状態から生じるパスの少なくとも1つで $\varphi$ が有効なものがある。

他の表現:

• 作用素 R は V で表記されることがある。
• 作用素 W は weak until を意味する。$fWg$ は $fUg\vee Gf$ と等価である。

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

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

様々な時相論理

• テンプレート:仮リンク (ITL)
• テンプレート:仮リンク
  • テンプレート:仮リンク (HML)
  • テンプレート:仮リンク
    • 計算木論理 (CTL)
    • 線形時相論理 (LTL)
    • Metric Interval Temporal Logic (MITL)
    • Signal Temporal Logic (STL)

時相論理と密接に関連する論理として、トポロジーや場所や空間的位置を扱う様相論理がある。

参考文献

• Mordechai Ben-Ari, Zohar Manna, Amir Pnueli: The Temporal Logic of Branching Time. POPL 1981: 164-176
• Amir Pnueli: The Temporal Logic of Programs FOCS 1977: 46-57
• 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
• テンプレート:Citation preprint

関連文献

• テンプレート:Cite book

関連項目

• オートマトン
• チョムスキー階層
• 状態遷移系
• 様相論理

外部リンク

• Temporal Logic by Yde Venema, formal description of syntax and semantics, questions of axiomatization. Treating also Kamp's dyadic temporal operators (since, until)
• Notes on games in temporal logic by Ian Hodkinson, including a formal description of first-order temporal logic
• CADP - provides generic model checkers for various temporal logic
• PAT is a powerful free model checker, LTL checker, simulator and refinement checker for CSP and its extensions (with shared variable, arrays, wide range of fairness).