時相論理
時相論理（Temporal Logic）とは、時間との関連で問題を理解し表現するための規則と表記法の体系である。時相論理では、「私はいつも腹ペコだ」、「私はそのうち腹ペコになる」、「私は何かを食べるまで腹ペコだろう」といった文を表現できる。1950年代末にアーサー・プライアーが提唱した様相論理に基づいた時相論理を特に時制論理（Tense Logic）と呼ぶことがある。ハンス・カンプが重要な業績を残した。その後、そこから発展し、アミール・プヌーリら計算機科学者や論理学者が研究を進めた。
時相論理はシステムのハードウェアやソフトウェアの要求仕様を記述する方法として形式的検証で利用される。例えば、「要求が発生したら常にリソースへのアクセスがそのうちに承認される。ただし、決して2つの要求を同時に承認してはならない」といった文章は時相論理で表せる。
概要
「私は腹ペコだ」という文を考えてみよう。この文の意味は時間経過に関わらず一定であるが、その真偽は時間経過によって変化する。あるときは真だし、またあるときは偽である。しかし、同時に真でもあり偽でもあるということはありえない。時相論理では、時と共に真理値の変化する文を扱う。非時相論理では、時間経過によって真理値が変化しない文しか扱えない。
時相論理は常に時系列について判断する能力を有する。線形時間論理（Linear Time Logic）と呼ばれるものはこの種の推論に限定されている。分岐論理（Branching Logic）は複数の時系列を判断できる。これは予測不能な挙動を示す環境を前提とする。さらに言えば、分岐論理では「私が永遠に腹ペコのままでいる可能性がある」といった文が表現可能である。他にも「私がもう腹ペコではなくなる可能性がある」という文も表現可能である。「私」が食べ物にありつけるかどうか不明ならば、これらの文はどちらも真である。
歴史
アリストテレスは主に三段論法を研究したが、現代の時相論理のような研究もしており、一階時相二値論理のような形式を部分的に検討したことがある。特に不確定な未来の事象を扱う際、アリストテレスは二値の意味論を適用できないと考え、例えば「明日、海戦が勃発するだろう」といった文の真偽を現時点で決定できないとした[1]。
その後数千年間、ほとんど発展は見られなかった。19世紀、チャールズ・サンダース・パースは次のように記している。
| 「 | 時間は、論理学者にとって論理外のものとみなされてきた。私は決してこの意見に与しない。しかし論理学はそこまでの状態に達しておらず、今の論理を時相を扱えるよう修正すれば大きな混乱を生じるであろう。私の思考もまだその段階に達していない。 | 」 |
アーサー・プライアーは自由意志や予定説といった哲学的問題を検討した。彼の妻によれば、彼が最初に時相論理を定式化したのは1953年のことだという。1955年から56年にかけてオックスフォード大学でそれについて講義をし、1957年には Time and Modality を出版。その中で2つの時相接続子（様相作用素）F（「未来のいずれかの時点で」の意）とP（「過去のいずれかの時点で」の意）を備えた命題様相論理を説明している。この先駆的取り組みで、プライアーは時間を線型なものとみなしている。しかし1958年、ソール・クリプキはプライアーへの手紙で、その仮定は不当だと指摘した。計算機科学での同様な考え方を予示しつつ、プライアーは熟慮の上それを採用し2つの分岐時間の理論を考案、"Ockhamist" と "Peircean" と名付けた[2]。1958年から1965年にかけて、プライアーは Charles Leonard Hamblin と共同で時相論理について研究した。1967年、時相論理に関する研究の集大成として Past, Present, and Future を出版。その2年後に亡くなった[3]。
ハンス・カンプは1968年の博士論文で二値の時相作用素 Since と Until を導入し[4]、その論文で時相論理と一階述語論理を関連付ける重要な考察も行い、それが「カンプの定理」と呼ばれるようになった[5][2][6]。
形式的検証では、線形時相論理（アミール・プヌーリによる線形時間論理の一種）と計算木論理（エドムンド・クラークとアレン・エマーソンによる分岐時間論理の一種）が競っている。後者のほうが分岐を扱えるぶんだけ前者よりも効果的であると指摘されることがある。エマーソンと Lei は、いかなる線形論理も複雑性を変えずに分岐論理に拡張可能であることを示した。
時相作用素
時相論理では2種類の作用素を使用する。論理作用素と様相作用素である[1]。論理作用素は一般的な真理関数作用素である([math]\neg,\or,\and,\rightarrow[/math])。線形時相論理や計算木論理で使用される様相作用素を以下に示す。
| 文字表記 | 記号表記 | 定義 | 説明 | ダイアグラム |
|---|---|---|---|---|
| 二項演算 | ||||
| [math]\phi[/math] U [math]\psi[/math] | [math]\phi ~\mathcal{U}~ \psi[/math] | [math]\begin{matrix}(B\,\mathcal{U}\,C)(\phi)= \\ (\exists i:C(\phi_i)\land(\forall j\lt i:B(\phi_j)))\end{matrix}[/math] | Until: [math]\psi[/math] は現在あるいは未来の位置で有効で、[math]\phi[/math] はそれ以前の位置まで有効でなければならない。その位置で [math]\phi[/math] は保持する必要はなくなる。 |  |
| [math]\phi[/math] R [math]\psi[/math] | [math]\phi ~\mathcal{R}~ \psi[/math] | [math]\begin{matrix}(B\,\mathcal{R}\,C)(\phi)= \\ (\forall i:C(\phi_i)\lor(\exists j\lt i:B(\phi_j)))\end{matrix}[/math] | Release: [math]\phi[/math] が真である最初の位置まで [math]\psi[/math] が真であるならば（またはそのような位置がないなら永久に）、[math]\phi[/math] は [math]\psi[/math] をリリースする。 |  |
| 単項演算 | ||||
| N [math]\phi[/math] | [math]\circ \phi[/math] | [math]\mathcal{N}B(\phi_i)=B(\phi_{i+1})[/math] | Next: [math]\phi[/math] は次の状態で有効でなければならない。（X は同義語的に使われる） |  |
| F [math]\phi[/math] | [math]\Diamond \phi[/math] | [math]\mathcal{F}B(\phi)=(true\,\mathcal{U}\,B)(\phi)[/math] | Finally: [math]\phi[/math] は結局、有効となる必要がある。（将来のいずれかの時点で） |  |
| G [math]\phi[/math] | [math]\Box \phi[/math] | [math]\mathcal{G}B(\phi)=\neg\mathcal{F}\neg B(\phi)[/math] | Globally: [math]\phi[/math] はその後ずっと有効である必要がある。 |  |
| A [math]\phi[/math] | [math]\forall \phi[/math] | [math]\begin{matrix}(\mathcal{A}B)(\psi)= \\ (\forall \phi:\phi_0=\psi\to B(\phi))\end{matrix}[/math] | All: [math]\phi[/math] は現在状態から生ずる全てのパス上で有効である必要がある。 | |
| E [math]\phi[/math] | [math]\exists \phi[/math] | [math]\begin{matrix}(\mathcal{E}B)(\psi)= \\ (\exists \phi:\phi_0=\psi\land B(\phi))\end{matrix}[/math] | Exists: 現在状態から生じるパスの少なくとも1つで [math]\phi[/math] が有効なものがある。 | |
他の表現:
- 作用素 R は V で表記されることがある。
- 作用素 W は weak until を意味する。[math]f W g[/math] は [math]f U g \or G f [/math] と等価である。
B([math]\phi[/math]) が整論理式(wff)であれば、単項作用素は全て整論理式である。B([math]\phi[/math]) と C([math]\phi[/math]) が整論理式であれば、二項作用素は全て整論理式である。
論理体系によっては一部の作用素は表現できない。例えば、Temporal Logic of Actions では N 作用素は表現できない。
様々な時相論理
- インターバル時相論理 (ITL)
- μ計算
時相論理と密接に関連する論理として、トポロジーや場所や空間的位置を扱う様相論理がある[9][10]。
脚注
- ↑ Vardi 2008, p. 153.
- ↑ 2.0 2.1 Vardi 2008, p. 154.
- ↑ (1995) Temporal logic: from ancient ideas to artificial intelligence. Springer. ISBN 978-0-7923-3586-3. pp. 176-178, 210
- ↑ http://plato.stanford.edu/entries/logic-temporal/M
- ↑ (2008) Modalities and Multimodalities. Springer. ISBN 978-1-4020-8589-5.
- ↑ (2009) Reasoning Web. Semantic Technologies for Information Systems: 5th International Summer School 2009, Brixen-Bressanone, Italy, August 30 - September 4, 2009, Tutorial Lectures. Springer. ISBN 978-3-642-03753-5.
- ↑ O. Maler, D. Nickovic, "Monitoring temporal properties of continuous signals", 2004
- ↑ O. Maler, D. Nickovic, "Monitoring temporal properties of continuous signals", 2004
- ↑ Nicholas Rescher, James Garson, "Topological Logic" in The Journal of Symbolic Logic, 33(4):537-548, December, 1968
- ↑ Georg Henrik von Wright, "A Modal Logic of Place", in E. Sosa (Editor), pp. 65-73, "The Philosophy of Nicholas Rescher: Discussion and Replies", D. Reidel, Dordrecht, Holland, 1979
参考文献
- 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
- Moshe Y. Vardi (2008), “From Church and Prior to PSL”, in Orna Grumberg, Helmut Veith, 25 years of model checking: history, achievements, perspectives, Springer, ISBN 978-3-540-69849-4 preprint
関連文献
- (1995) Temporal logic: from ancient ideas to artificial intelligence. Springer. ISBN 978-0-7923-3586-3.
関連項目
外部リンク
- Temporal Logic （英語） - スタンフォード哲学百科事典「時相論理」の項目。
- 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).