時相論理

時相論理（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]。論理作用素は一般的な真理関数作用素である(${\displaystyle \neg ,\lor ,\land ,\rightarrow }$)。線形時相論理や計算木論理で使用される様相作用素を以下に示す。

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

他の表現:

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

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

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

• インターバル時相論理（英語版） (ITL)
• μ計算（英語版）
  • ヘネシー・ミルナー論理（英語版） (HML)
  • CTL*（英語版）
    • 計算木論理 (CTL)
    • 線形時相論理 (LTL)
    • Metric Interval Temporal Logic (MITL) ^[7]
    • Signal Temporal Logic (STL) ^[7]

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

• 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

• Peter Øhrstrøm; Per F. V. Hasle (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).

表 話 編 歴 論理学
関連項目 学術的領域 議論学 価値論 批判的思考 再帰理論 形式意味論 論理史 非形式論理学 計算機科学における論理学（英語版） 数理論理学 数学 メタ論理学 メタ数学 モデル理論 哲学的論理学 哲学 論理学の哲学 数学の哲学 証明論 集合論 論理学の歴史 基本概念 アブダクション 分析的と総合的の区別（英語版） 二律背反 アプリオリ 演繹 定義(内包と外延) 記述 帰納 推論 論理的帰結 論理形式（英語版） 論理的含意（英語版） 論理的真理 名前 必要十分条件 意味 パラドックス 可能世界論 前提 確率 理性 推理 参考 意味論 命題 サブスティトゥーション（英語版） 統語論（英語版） 真理 真理値 妥当性 数学記号の表
哲学的論理学 批判的思考と非形式論理学 分析 曖昧 信念 信用性（英語版） 根拠 説明 説明力（英語版） 事実 誤謬 探究 意見 節約 根拠 プロパガンダ 思慮分別（英語版） 推理 関連 修辞学 厳格 漠然（英語版） 論理学の哲学 構成主義 真矛盾主義 虚構主義（英語版） 有限主義（英語版） 形式主義 直観主義 論理的原子論（英語版） 論理主義 唯名論 プラトニック実在論（英語版） プラグマティズム 実在論
メタ論理学と超数学 カントールの定理 決定問題 チャーチのテーゼ 無矛盾性 実効的方法（英語版） 数学基礎論 ゲーデルの完全性定理 ゲーデルの不完全性定理 健全性 完全性 決定可能性 解釈 レーヴェンハイム-スコーレムの定理 メタ定理（英語版） 充足可能性 独立性（英語版） 独立 タイプとトークンの区別 使用と言及の区別
数理論理学 基幹 形式言語 構成規則 形式体系 演繹システム（英語版） 形式的証明 形式意味論 論理式 集合 元 クラス 古典論理 公理 自然演繹 推論規則 有限関係（英語版） 定理 論理的帰結 公理系 型理論 記号 統語論（英語版） 理論（英語版） 名辞論理学（英語版） 命題 推論 論証 妥当性 三段論法 反対の正方形 ベン図 命題論理とブール論理 ブール関数 命題論理 論理演算 真理値表 原子論理式 リテラル 述語論理 量化 全称記号 存在記号 一階述語論理 二階述語論理 高階述語論理 単項述語計算（英語版） 標準形 連言標準形 選言標準形 否定標準形 冠頭標準形 スコーレム標準形 節標準形 集合論 集合 空集合 数え上げ 外延 有限集合 関数 部分集合 冪集合 可算集合 帰納的集合 定義域 値域 順序対 非可算集合 モデル理論 モデル（英語版） 解釈（英語版） 超準モデル 有限モデル理論 真理値 妥当性 証明論 形式的証明 演繹システム（英語版） 形式体系 定理 論理的帰結 推論規則 統語論（英語版） 再帰理論 再帰 帰納的集合 帰納的可算集合 決定問題 チャーチ＝チューリングのテーゼ 計算可能関数 原始再帰関数 表現 真理値表 クワイン・マクラスキー法 カルノー図 存在グラフ 概念地図 オイラー図 ベン図 スパイダー図 タブローの方法 Xバー理論 構文木 構文解析
非古典論理 様相論理学 真理様相（英語版） 価値様相（英語版） 義務論理 信念様相（英語版） 認識論理 時相論理 線形時相論理 直観主義 直観論理 構成的解析（英語版） ハイディング算術（英語版） 直観主義型理論 構成的集合論（英語版） ファジィ論理 真理の程度（英語版） ファジィルール（英語版） ファジィ集合 ファジィ有限要素（英語版） ファジィ集合演算（英語版） 部分構造論理 構造規則（英語版） 適切さの論理 線形論理 矛盾許容論理 真矛盾主義 様相記述論理（英語版） 存在論 オントロジー言語（英語版）
論理学者 アンダーソン アリストテレス イブン・ルシュド イブン・スィーナー ベイン（英語版） バーワイズ（英語版） ベルナイス ブール ブーロス（英語版） カントール カルナップ チャーチ クリュシッポス カリー ド・モルガン フレーゲ ギーチ ゲンツェン ゲーデル ヒルベルト クリーネ クリプキ ライプニッツ レーヴェンハイム（英語版） ペアノ パース パトナム クワイン ラッセル シュレーダー（英語版） スコトゥス スコーレム スマリヤン タルスキ チューリング ホワイトヘッド オッカムのウィリアム ウィトゲンシュタイン ツェルメロ
カテゴリ