時相論理のソースを表示

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

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

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

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

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

その後数千年間、ほとんど発展は見られなかった。19世紀、[[チャールズ・サンダース・パース]]は次のように記している。
{{Cquote|時間は、論理学者にとって論理外のものとみなされてきた。私は決してこの意見に与しない。しかし論理学はそこまでの状態に達しておらず、今の論理を時相を扱えるよう修正すれば大きな混乱を生じるであろう。私の思考もまだその段階に達していない。}}

{{仮リンク|アーサー・プライアー|en|Arthur Prior}}は[[自由意志]]や[[予定説]]といった哲学的問題を検討した。彼の妻によれば、彼が最初に時相論理を定式化したのは1953年のことだという。1955年から56年にかけて[[オックスフォード大学]]でそれについて講義をし、1957年には ''Time and Modality'' を出版。その中で2つの時相接続子（{{仮リンク|様相作用素|en|modal operator}}）F（「未来のいずれかの時点で」の意）とP（「過去のいずれかの時点で」の意）を備えた[[命題論理|命題]]様相論理を説明している。この先駆的取り組みで、プライアーは時間を線型なものとみなしている。しかし1958年、[[ソール・クリプキ]]はプライアーへの手紙で、その仮定は不当だと指摘した。計算機科学での同様な考え方を予示しつつ、プライアーは熟慮の上それを採用し2つの分岐時間の理論を考案、"Ockhamist" と "Peircean" と名付けた{{Sfn|Vardi|2008|p=154}}{{要説明|date=2011年4月}}。1958年から1965年にかけて、プライアーは [[:en:Charles Leonard Hamblin|Charles Leonard Hamblin]] と共同で時相論理について研究した。1967年、時相論理に関する研究の集大成として ''Past, Present, and Future'' を出版。その2年後に亡くなった<ref>{{Cite book|author1=Peter Øhrstrøm|author2=Per F. V. Hasle|title=Temporal logic: from ancient ideas to artificial intelligence|year=1995|publisher=Springer|isbn=978-0-7923-3586-3}} pp. 176-178, 210</ref>。

{{仮リンク|ハンス・カンプ|en|Hans Kamp}}は1968年の博士論文で二値の時相作用素 ''Since'' と ''Until'' を導入し<ref>http://plato.stanford.edu/entries/logic-temporal/M</ref>、その論文で時相論理と[[一階述語論理]]を関連付ける重要な考察も行い、それが「カンプの定理」と呼ばれるようになった<ref name="CarnielliPizzi2008">{{Cite book |author1=Walter Carnielli |author2=Claudio Pizzi |title=Modalities and Multimodalities |url= https://books.google.co.jp/books?id=XpAFM04G6BAC&pg=PA181&redir_esc=y&hl=ja |year=2008 |publisher=Springer |isbn=978-1-4020-8589-5 |page=181}}</ref>{{Sfn|Vardi|2008|p=154}}<ref name="TessarisFranconi2009">{{Cite book |author1=Sergio Tessaris |author2=Enrico Franconi |author3=Thomas Eiter |title=Reasoning Web. Semantic Technologies for Information Systems: 5th International Summer School 2009, Brixen-Bressanone, Italy, August 30 - September 4, 2009, Tutorial Lectures |url= https://books.google.co.jp/books?id=JdyeU7zs4-AC&pg=PA112&redir_esc=y&hl=ja |year=2009 |publisher=Springer |isbn=978-3-642-03753-5 |page=112}}</ref>。

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

==時相作用素==
時相論理では2種類の[[作用素]]を使用する。[[論理演算|論理作用素]]と{{仮リンク|様相作用素|en|modal operator}}である[http://plato.stanford.edu/entries/logic-temporal/]。論理作用素は一般的な[[真理関数]]作用素である(<math>\neg,\lor,\land,\rightarrow</math>)。線形時相論理や計算木論理で使用される様相作用素を以下に示す。

{| class="wikitable"
|-
! style="word-break: keep-all" | 文字表記
! style="word-break: keep-all" | 記号表記
! style="word-break: keep-all" | 定義
! style="word-break: keep-all" | 説明
! style="word-break: keep-all" | ダイアグラム
|-
| colspan="4" style="text-align: center" | [[二項演算]]
|-
| style="white-space:nowrap; text-align: center" | <math>\phi</math> '''U''' <math>\psi</math>
| style="text-align: center" | <math>\phi ~\mathcal{U}~ \psi</math>
| style="text-align: center" | <math>\begin{matrix}(B\,\mathcal{U}\,C)(\phi)= \\ (\exists i:C(\phi_i)\land(\forall j<i:B(\phi_j)))\end{matrix}</math>
|'''U'''ntil: <math>\psi</math> は現在あるいは未来の位置で有効で、<math>\phi</math> はそれ以前の位置まで有効でなければならない。その位置で <math>\phi</math> は保持する必要はなくなる。
|<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>
|-
| style="white-space:nowrap; text-align: center" | <math>\phi</math> '''R''' <math>\psi</math>
| style="text-align: center" | <math>\phi ~\mathcal{R}~ \psi</math>
| style="text-align: center" | <math>\begin{matrix}(B\,\mathcal{R}\,C)(\phi)= \\ (\forall i:C(\phi_i)\lor(\exists j<i:B(\phi_j)))\end{matrix}</math>
|'''R'''elease: <math>\phi</math> が真である最初の位置まで <math>\psi</math> が真であるならば（またはそのような位置がないなら永久に）、<math>\phi</math> は <math>\psi</math> をリリースする。
|<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>
|-
| colspan="4" style="text-align: center" | [[単項演算]]
|-
| style="white-space:nowrap; text-align: center" | '''N''' <math>\phi</math>
| style="text-align: center" | <math>\circ \phi</math>
| style="text-align: center" | <math>\mathcal{N}B(\phi_i)=B(\phi_{i+1})</math>
|'''N'''ext: <math>\phi</math> は次の状態で有効でなければならない。（'''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>
|-
| style="white-space:nowrap; text-align: center" | '''F''' <math>\phi</math>
| style="white-space:nowrap; text-align: center" | <math>\Diamond \phi</math>
| style="white-space:nowrap; text-align: center" | <math>\mathcal{F}B(\phi)=(true\,\mathcal{U}\,B)(\phi)</math>
|'''F'''inally: <math>\phi</math> は結局、有効となる必要がある。（将来のいずれかの時点で）
|<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>
|-
| style="white-space:nowrap; text-align: center" | '''G''' <math>\phi</math>
| style="text-align: center" | <math>\Box \phi</math>
| style="text-align: center" | <math>\mathcal{G}B(\phi)=\neg\mathcal{F}\neg B(\phi)</math>
|'''G'''lobally: <math>\phi</math> はその後ずっと有効である必要がある。
|<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>
|-
| style="white-space:nowrap; text-align: center" | '''A''' <math>\phi</math>
| style="text-align: center" | <math>\forall \phi</math>
|  style="text-align: center" | <math>\begin{matrix}(\mathcal{A}B)(\psi)= \\ (\forall \phi:\phi_0=\psi\to B(\phi))\end{matrix}</math>
|'''A'''ll: <math>\phi</math> は現在状態から生ずる全てのパス上で有効である必要がある。
|
|-
| style="white-space:nowrap; text-align: center" | '''E''' <math>\phi</math>
| style="text-align: center" |<math>\exists \phi</math>
|  style="text-align: center" | <math>\begin{matrix}(\mathcal{E}B)(\psi)= \\ (\exists \phi:\phi_0=\psi\land B(\phi))\end{matrix}</math>
|'''E'''xists: 現在状態から生じるパスの少なくとも1つで <math>\phi</math> が有効なものがある。
|
|}

他の表現:
* 作用素 '''R''' は '''V''' で表記されることがある。
* 作用素 '''W''' は ''weak until'' を意味する。<math>f W g</math> は <math>f U g \lor G f </math> と等価である。

B(<math>\phi</math>) が[[well-formed formula|論理式]](wff)であれば、単項作用素は全て論理式である。B(<math>\phi</math>) と C(<math>\phi</math>) が論理式であれば、二項作用素は全て論理式である。

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

== 様々な時相論理 ==
* {{仮リンク|インターバル時相論理|en|Interval temporal logic}} (ITL)
* {{仮リンク|μ計算|en|mu calculus}}
** {{仮リンク|ヘネシー・ミルナー論理|en|Hennessy-Milner logic}} (HML)
** {{仮リンク|CTL*|en|CTL*}}
*** [[計算木論理]] (CTL)
*** [[線形時相論理]] (LTL)
*** Metric Interval Temporal Logic (MITL) <ref name="#1"> O. Maler, D. Nickovic, "Monitoring temporal properties of continuous signals", 2004</ref>
*** Signal Temporal Logic (STL) <ref name="#1"/>

時相論理と密接に関連する論理として、トポロジーや場所や空間的位置を扱う[[様相論理]]がある<ref>Nicholas Rescher, James Garson, "Topological Logic" in The Journal of Symbolic Logic, 33(4):537-548, December, 1968</ref><ref>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</ref>。

== 脚注 ==
{{Reflist}}

== 参考文献 ==
* 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 |editor=Orna Grumberg, Helmut Veith |title=25 years of model checking: history, achievements, perspectives |year=2008 |publisher=Springer |isbn=978-3-540-69849-4 |chapter=From [[アロンゾ・チャーチ|Church]] and Prior to [[Property Specification Language|PSL]]|author=Moshe Y. Vardi |ref={{SfnRef|Vardi|2008}}}} [http://www.cs.rice.edu/~vardi/papers/25mc.ps.gz preprint] 

== 関連文献 ==
* {{Cite book|author1=Peter Øhrstrøm|author2=Per F. V. Hasle|title=Temporal logic: from ancient ideas to artificial intelligence|year=1995|publisher=Springer|isbn=978-0-7923-3586-3}}

== 関連項目 ==
* [[オートマトン]]
* [[チョムスキー階層]]
* [[状態遷移系]]
* [[様相論理]]

==外部リンク==
{{SEP|logic-temporal|Temporal Logic}}

*[http://staff.science.uva.nl/~yde/papers/TempLog.pdf Temporal Logic] by Yde Venema, formal description of syntax and semantics, questions of axiomatization. Treating also Kamp's dyadic temporal operators (since, until)
*[http://www.doc.ic.ac.uk/~imh/papers/sa.ps.gz Notes on games in temporal logic] by Ian Hodkinson, including a formal description of first-order temporal logic
*[http://www.inrialpes.fr/vasy/cadp CADP - provides generic model checkers for various temporal logic]
*[http://www.comp.nus.edu.sg/~pat/ 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).

{{Logic}}

{{DEFAULTSORT:しそうろんり}}
[[Category:時相論理|*]]
[[Category:形式手法]]
[[Category:数理論理学]]
[[Category:論理学]]
[[Category:時空の哲学]]
[[Category:数学に関する記事]]