時間論理

論理学において、時間論理とは、時間に関して限定された命題（例えば、「私はいつも空腹だ」、「私はいずれ空腹になるだろう」、「私は何かを食べるまで空腹のままだろう」など）を表現し、推論するための規則と記号体系のことである。

時間論理は形式検証において重要な応用例を見出しており、ハードウェアまたはソフトウェアシステムの要件を記述するために用いられます。例えば、要求があった場合には必ずリソースへのアクセスが最終的に許可されるが、同時に2つの要求者にアクセスが許可されることは決してない、といったことを記述したい場合、時間論理を用いることで容易に表現できます。

時間論理という用語は、時制論理、すなわち1950年代後半にアーサー・プライアーによって導入され、ハンス・カンプが重要な貢献をした様相論理に基づく時間論理体系を指す場合にも用いられることがある。これは、アミール・プヌエリをはじめとするコンピュータ科学者や論理学者によってさらに発展させられてきた。

モチベーション

「私はお腹が空いている」という文を考えてみましょう。その意味は時間的に一定ですが、真偽値は時間とともに変化する可能性があります。真である場合もあれば偽である場合もありますが、真偽が同時に存在することはありません。時間論理では、文の真偽値は時間とともに変化します。これに対し、非時間論理は、真偽値が時間的に一定の文にのみ適用されます。このように、真偽値を時間とともに扱う点が、時間論理と計算動詞論理を区別する特徴です。

時間論理は常に時間軸に関する推論能力を備えています。いわゆる「線形時間」論理は、この種の推論に限定されます。一方、分岐時間論理は複数の時間軸に関する推論が可能です。これにより、特に予測不可能な動作をする可能性のある環境を扱うことができます。例を続けると、分岐時間論理では、「私は永遠に空腹のままである可能性がある」と「最終的に空腹ではなくなる可能性がある」という文を述べることができます。私がいつか食事を与えられるかどうか分からない場合、これらの文は両方とも真となり得ます。

歴史

アリストテレスの論理学はほぼ完全に定言三段論法の理論に関係しているが、彼の著作には時間論理の先駆けと見なされている箇所があり、初期の部分的に発達した一階時間様相二値論理を示唆している可能性がある。アリストテレスは特に未来の偶発事象の問題に関心を寄せており、二値原理が未来の出来事に関する命題、つまり「明日海戦がある」といった未来の出来事に関する命題が真か偽かを現時点で判断できるという考えを受け入れることができなかった。^{[ 1 ]}

19世紀のチャールズ・サンダース・パースは、アーサー・プライアーの研究以前は、何千年もの間ほとんど発展がなかったと指摘している。 ^[²^]

論理学者たちは通常、時間をいわゆる「論理外」の要素とみなしてきた。私はこの意見に賛同したことはない。しかし、論理学は、その形式に時間的な修正を導入すると大きな混乱を招くような段階にはまだ達していないと考えてきたし、今でもその考えは変わらない。

時間論理の最初の体系は、1947 年にポーランドの論理学者イェジー・ウォシによって発表されました。^{[ 3 ]}彼の著書『Podstawy Analizy Metodologicznej Kanonów Milla』（ミルの方法の方法論的分析の基礎）の中で、彼はミルの規範の形式化を提示しました。ウォシのアプローチでは、時間要素に重点が置かれました。そのため、彼の目標を達成するために、彼は時間関数の形式化の手段を提供できる論理を作成する必要がありました。この論理は、ウォシの主な目的の副産物と見なすことができますが、^{[ 4 ]}後にウォシの認識論理の発明の枠組みとして使用された最初の位置論理でした。この論理自体は、様相演算子を使用するプライアーの時制論理とは構文が大きく異なります。ウォシュの論理言語は、位置論理に特有の実現演算子を用いており、この演算子によって式は、その真偽値が考慮される特定の文脈と結び付けられる。ウォシュの研究では、この考慮される文脈は時間的なものに限られており、したがって式は特定の時点または時間間隔と結び付けられていた。

アーサー・プライアーは、自由意志と予定説の哲学的意味合いに関心を抱いていた。彼の妻によると、彼は1953年に初めて時間論理の形式化を検討した。彼の研究成果は、1954年にウェリントンで開催された会議で初めて発表された。 ^{[ 4 ]}プライアーが提示した体系は、構文的にはウォシュの論理に似ていたが、彼がウォシュの以前の研究に明示的に言及したのは、プライアーの『形式論理』の付録1の最後のセクションで、1955年になってからだった。^{[ 4 ]}時制論理に加えて、プライアーはいくつかの位置論理体系を構築したが、それらはウォシュから主要なアイデアを受け継いでいた。^{[ 5 ]}

プライアーは1955年から1956年にかけてオックスフォード大学でこのテーマに関する講義を行い、1957年に『時間と様相』を出版した。この中で彼は、「未来のある時点」と「過去のある時点」に対応する2つの時間結合子（様相演算子）FとPを持つ命題様相論理を導入した。この初期の著作では、プライアーは時間を線形であると考えていた。しかし1958年、彼はソール・クリプキから手紙を受け取り、この仮定はおそらく不当であると指摘された。コンピュータ科学における同様の展開を予見させる展開として、プライアーはこれを考慮に入れ、「オッカム主義」と「パース主義」と呼ばれる2つの分岐時間理論を開発した。^[²^] 1958年から1965年の間にプライアーはチャールズ・レナード・ハンブリンとも文通しており、この分野における初期の発展のいくつかは、例えばハンブリン含意など、この文通に遡ることができる。プライアーは、このテーマに関する最も成熟した著作である『過去、現在、未来』を1967年に出版した。彼はその2年後に亡くなった。^[⁶^]

位置的時制論理の研究は、1960年代と1970年代にニコラス・レシャーによって続けられた。彼は、 『時間論理に関する覚書』（1966年）、『時間命題の論理について』（1968年） 、『位相論理』（1968年）、『時間論理』（1971年）などの著作で、ウォシュとプライアーの体系間の関連性を研究した。さらに、プライアーの時制演算子は、特定の位置論理における実現演算子を用いて定義できることを証明した。 ^{[ 5 ]}レシャーは、その研究において、より一般的な位置論理体系も構築した。最初の体系は純粋に時間的な用途のために構築されたものであったが、彼は、実現演算子を含むことを意図しているが、時計公理のような特定の時間公理を持たない論理に対して、位相論理という用語を提案した。

二項時間演算子SinceとUntil は、ハンス・カンプが1968 年の博士論文^{[ 7 ]}で導入したもので、時間論理と一階述語論理を関連付ける重要な結果も含まれており、これは現在カンプの定理として知られています。^{[ 8 ]}^{[ 2 ]}^{[ 9 ]}

形式検証の初期の有力候補は、アミール・プヌエリによる線形時間論理である線形時相論理と、モルデカイ・ベン＝アリ、ゾハル・マンナ、アミール・プヌエリによる分岐時間論理である計算木論理（CTL）であった。CTLとほぼ同等の形式体系が、ほぼ同時期にEMクラークとEAエマーソンによって提案された。2番目の論理が最初の論理よりも効率的に判定できるという事実は、時折主張されるように、分岐時間論理と線形時間論理全般を反映するものではない。むしろ、エマーソンとレイは、任意の線形時間論理を、同じ計算量で判定できる分岐時間論理に拡張できることを示している。

ウォシュの位置論理

Łośの論理学は、1947 年の修士論文Podstawy Analizy Metodologicznej Kanonów Milla (ミルの方法論的分析の基礎) として発表された。^{[ 10 ]}彼の哲学的および形式的概念は、指導教官がヤン・ウカシェヴィチの弟子であるイェジー・スウペツキであったことから、リヴィウ・ワルシャワ学派の論理学の継続と見なすことができる。この論文は 1977 年まで英語に翻訳されなかったが、ヘンリク・ヒジュは1951 年にJournal of Symbolic Logicに簡潔だが有益なレビューを発表した。このレビューにはŁośの研究の中核概念が含まれており、論理学界で彼の成果を普及させるのに十分であった。この研究の主な目的は、ミルの規範を形式論理の枠組みで提示することであった。この目的を達成するために、著者はミルの概念構造における時間的機能の重要性を研究した。そして、ミルの規範とその時間的側面を枠組みとして適合する公理的論理体系を提示した。

構文

『ミルの方法論的分析の基礎』（Podstawy Analizy Metodologicznej Kanonów Milla）で最初に発表された論理の言語は、以下のものから構成されていた。 ^[³^]

1階論理演算子 '¬'、'∧'、'∨'、'→'、'≡'、'∀'、'∃'
実現演算子 U
機能記号 δ
命題変数 p ₁、p ₂、p ₃、...
時刻 t ₁、t ₂、t ₃、...を表す変数
時間間隔を表す変数 n ₁、n ₂、n ₃、...

項の集合（Sで表される）は、次のように構成される。

時間的瞬間または時間間隔を表す変数は、
もし $\tau \in S$ そして $\epsilon$ 時間間隔変数である場合、 $\delta (\tau ,\epsilon )\in S$

式のセット（以下で示される） ${\text{For}}$ ）は次のように構築されます：^{[ 10 ]}

すべての一階論理式は ${\text{For}}$
もし $\tau \in S$ そして $\phi$ は命題変数であるならば、 $U_{\tau }(\phi )\in {\text{For}}$
もし $\phi \in For$ 、それから $\neg \phi \in {\text{For}}$
もし $\phi ,\psi \in {\text{For}}$ そして $\circ \in \{\wedge ,\vee ,\rightarrow ,\equiv \}$ 、それから $\phi \circ \psi \in {\text{For}}$
もし $\phi \in {\text{For}}$ そして $Q\in \{\forall ,\exists \}$ そして $\upsilon$ が命題変数、モーメント変数、または区間変数である場合、 $Q_{\upsilon }\phi \in {\text{For}}$

オリジナルの公理系

$U_{t_{1}}\neg p_{1}\equiv \neg U_{t_{1}}p_{1}$
$U_{t_{1}}(p_{1}\rightarrow p_{2})\rightarrow (U_{t_{1}}p_{1}\rightarrow U_{t_{1}}p_{2})$
$U_{t_{1}}((p_{1}\rightarrow p_{2})\rightarrow ((p_{2}\rightarrow p_{3})\rightarrow (p_{1}\rightarrow p_{3})))$
$U_{t_{1}}(p_{1}\rightarrow (\neg p_{1}\rightarrow p_{2}))$
$U_{t_{1}}((\neg p_{1}\rightarrow p_{1})\rightarrow p_{1})$
$\forall _{t_{1}}U_{t_{1}}p_{1}\rightarrow p_{1}$
$\forall _{t_{1}}\forall _{n_{1}}\exists _{t_{2}}\forall _{p_{1}}(U_{\delta (t_{1},n_{1})}p_{1}\equiv U_{t_{2}}p_{1})$
$\forall _{t_{1}}\forall _{n_{1}}\exists _{t_{2}}\forall _{p_{1}}(U_{\delta (t_{2},n_{1})}p_{1}\equiv U_{t_{1}}p_{1})$
$\forall _{t_{1}}\exists _{p_{1}}\forall _{t_{2}}(U_{t_{2}}p_{1}\equiv \forall _{p_{2}}(U_{t_{1}}p_{2}\equiv U_{t_{2}}p_{2}))$

プライアーの時制論理（TL）

『時間と様相』で導入された文時制論理には、（一階命題論理における通常の真理関数演算子に加えて） 4つの（非真理関数的な）様相演算子がある。^[¹¹^]

P：「それは…であった」（Pは「過去」の略）
F：「～となるだろう…」（Fは「未来」の略）
G：「それはいつだって変わらないだろう…」
H：「昔からずっとそうだったんです…」

πを無限経路とすれば、これらを組み合わせることができます。 ^{[ 12 ]}

$\pi \vDash FG\phi$ 「ある時点で、 $\phi$ 「パスの将来のすべての状態において真である」
$\pi \vDash GF\phi$ : " $\phi$ 「経路上の無限の数の状態において真である」

PとFからGとHを定義することができ、またその逆も可能である。

{\begin{aligned}F&\equiv \lnot G\lnot \\P&\equiv \lnot H\lnot \end{aligned}}

構文と意味論

TLの最小限の構文は、以下のBNF文法で規定される。

{\displaystyle \phi

ここで、aは何らかの原子式である。^{[ 13 ]}

TL では、クリプキモデルを使用して文の真偽を評価します。集合TとT上の二項関係< (「優先順位」と呼ばれる) のペア ( T 、 <) をフレームと呼びます。モデルは、フレームの3 つ ( T、 <、V ) と、原子式と時間値の各ペア ( a、u ) に何らかの真偽値を割り当てる評価と呼ばれる関数Vによって与えられます。「 ϕは、時刻uにおいてモデルU =( T、 <、V ) で真である」という概念は、 U ⊨ ϕ [ u ]と略記されます。この表記法では、^[¹⁴^]

フレームのクラスFが与えられたとき、 TL の文ϕは

Fに関して有効であるのは、すべてのモデルU = ( T ,<, V ) に対して ( T ,<)がFに含まれ、すべてのu がTに含まれる場合、U ⊨ ϕ [ u ]が成り立つ場合である。
Fに関して充足可能であるとは、 Fに含まれる( T ,<) を持つモデルU =( T ,<, V ) が存在し、Tに含まれるあるuに対して、 U ⊨ ϕ [ u ]が成り立つ場合をいう。
Fに関する文ψの結果とは、 Fに含まれる ( T ,<)を持つすべてのモデルU =( T ,<, V ) と、 Tに含まれるすべてのuに対して、U ⊨ ψ [ u ]ならばU ⊨ ϕ [ u ]であるようなものである。

多くの文は、限られた種類のフレームに対してのみ有効です。一般的には、関係 < が推移的、反対称的、反射的、三分法的、非反射的、全結合的、稠密、またはこれらの組み合わせであるものに限定して、フレームの種類を限定します。

最小限の公理的論理

バージェスは、関係 < について何の仮定も置かず、意味のある推論を可能にする論理を、次の公理図式に基づいて概説している。^{[ 15 ]}

Aは一階述語論理のトートロジーである。
G( A → B )→(G A →G B )
H( A → B )→(H A →H B )
A →GP A
A →HF A

以下の推論規則に従う。

A → BおよびAが与えられた場合、B (法則)を推定します。
トートロジーAが与えられたとき、G Aを推論する
トートロジーAが与えられたとき、H Aを推論する

以下の規則を導き出すことができる。

ベッカーのルール：A → Bが与えられたとき、T A → T Bを推論する。ここで T は時制であり、G、H、F、P から構成される任意のシーケンスである。
ミラーリング：定理Aが与えられたとき、G を H に置き換える（したがって F を P に置き換える）ことによって得られるミラーステートメントA ^{§を導き、その逆も行う。}
双対性：定理Aが与えられたとき、∧ を ∨ と、G を F と、H を P と入れ替えることによって得られる双対命題A * を導出する。

述語論理への翻訳

バージェスは、TL のステートメントから、1 つの自由変数x ₀ (現在を表す)を持つ一階述語論理のステートメントへのメレディス変換を与えている。この変換Mは、次のように再帰的に定義される。 ^[¹⁶^]

{\begin{aligned}&M(a)&&=a^{*}x_{0}\\&M(\lnot \phi )&&=\lnot M(\phi )\\&M(\phi \land \psi )&&=M(\phi )\land M(\psi )\\&M({\mathsf {G}}\phi )&&=\forall x_{1}(x_{0}<x_{1}\rightarrow M(A^{+}))\\&M({\mathsf {H}}\phi )&&=\forall x_{1}(x_{1}<x_{0}\rightarrow M(A^{+}))\end{aligned}}

どこ $A^{+}$ すべての変数インデックスが 1 ずつ増加した文 $Aであり、$ $a^{*}$ は、次のように定義される一項述語である。 $x\mapsto V(a,x)$ 。

時間演算子

時間論理には、論理演算子と様相演算子の 2 種類の演算子があります。 ^{[ 17 ]}論理演算子は通常の真理関数演算子です ( $\neg ,\lor ,\land ,\rightarrow$ ) 線形時相論理および計算木論理で使用される様相演算子は、次のように定義されます。

代替記号:

演算子RはVで表されることもある。
演算子Wは弱い until演算子です。 $f\mathbf {W} g$ と同等 $f\mathbf {U} g\lor \mathbf {G} f$

単項演算子は、 $B($ $φ$ $)$ が整形式であれば整形式である。二項演算子は $、B($ $φ$ $)$ と $C($ $φ$ $)$ が整形式であれば整形式である。

論理体系によっては、表現できない演算子が存在する。例えば、N演算子は、動作の時間論理では表現できない。

時間論理

時間論理には以下が含まれます。

位置論理のいくつかの体系
線形時相論理（LTL）分岐タイムラインのない時相論理
計算ツリー論理（CTL）分岐タイムライン付き時相論理
区間時間論理（ITL）
行動の時間論理（TLA）
信号時間論理（STL）^{[ 18 ]}
タイムスタンプ時相論理（TTL）^{[ 19 ]}
物件仕様言語（PSL）
CTL* は、LTL と CTL を一般化したものです。
ヘネシー・ミルナー論理（HML）
モーダルμ計算は、HMLとCTL*を部分集合として含む。
メトリック時相論理（MTL）^{[ 20 ]}
メトリック間隔時相論理（MITL）^{[ 18 ]}
時間付き命題時相論理（TPTL）
切り詰められた線形時相論理(TLTL) ^{[ 21 ]}
ハイパーテンポラル論理（HyperLTL）^{[ 22 ]}

時間的、年代的、または時制的な論理と密接に関連する変種として、「トポロジー」、「場所」、「空間的位置」に基づく様相論理がある。^{[ 23 ]}^{[ 24 ]}

注記

↑ヴァルディ 2008、153ページ
1 2 3 Vardi 2008、p. 154
1 2 Łoś、イェジ（1947）。「ポドスタウィ分析方法論、ミラ」。Zasoby Biblioteki Głównej Umcs (ポーランド語)。ナクウ。 Uniwersytetu Marii Curie-Skłodowskiej。
1 2 3 Øhrstrøm, Peter (2019). 「近代時間論理の初期の歴史におけるANPriorとJerzy Łośの貢献の意義」 .時間の論理と哲学：Priorからのさらなるテーマ、第2巻. 時間の論理と哲学。ISBN 9788772102658。
1 2 Rescher, Nicholas; Garson, James (1969 年 1 月). "位相論理" . The Journal of Symbolic Logic . 33 (4): 537– 548. doi : 10.2307/2271360 . ISSN 0022-4812 . JSTOR 2271360 . S2CID 2110963 .
↑ Peter Øhrstrøm; Per FV Hasle (1995). Temporal logic: from ancient ideas to artificial intelligence . Springer. ISBN 978-0-7923-3586-3。176～178ページ、210ページ
↑ 「時間論理（スタンフォード哲学百科事典）」。Plato.stanford.edu 。 2014年7月30日取得。
↑ウォルター・カルニエリ、クラウディオ・ピッツィ（2008）。『モダリティとマルチモダリティ』。シュプリンガー。181ページ。ISBN 978-1-4020-8589-5。
↑ Sergio Tessaris; Enrico Franconi; Thomas Eiter (2009). Reasoning Web. Semantic Technologies for Information Systems: 5th International Summer School 2009, Brixen-Bressanone, Italy, August 30 – September 4, 2009, Tutorial Lectures . Springer. p. 112. ISBN 978-3-642-03753-5。
1 2トカチク、マルシン。ヤルムジェク、トマシュ (2019)。「Jerzy Łoś 位置微積分学と時間論理の起源」論理と論理哲学。28 (2): 259–276。土井: 10.12775/LLP.2018.013。ISSN 2300-9802。
↑ Prior, Arthur Norman (2003). Time and modality: the John Locke lectures for 1955–6, delivered at the University of Oxford . Oxford: The Clarendon Press. ISBN 9780198241584OCLC 905630146
↑ Lawford, M. (2004). "時間論理入門" (PDF) .マクマスター大学コンピュータサイエンス学部.
↑ゴランコ、ヴァレンティン; ガルトン、アントニー (2015). 「時間論理」。ザルタ、エドワード N. (編) 『スタンフォード哲学百科事典』（2015 年冬版）。スタンフォード大学形而上学研究室。
↑ミュラー、トーマス (2011)。「時制または時間論理」(PDF)。レオン・ホルステン編『哲学論理の連続体コンパニオン』A&C Black、329ページ。
↑バージェス、ジョン・P. (2009).哲学的論理学. プリンストン、ニュージャージー州: プリンストン大学出版局. p. 21. ISBN 9781400830497OCLC 777375659。
↑バージェス、ジョン・P. (2009).哲学的論理学. プリンストン、ニュージャージー州: プリンストン大学出版局. p. 17. ISBN 9781400830497OCLC 777375659。
↑ 「時間論理」。スタンフォード哲学百科事典。2020年2月7日。 2022年4月19日取得。
1 2 Maler, O.; Nickovic, D. (2004). "連続信号の時間的特性のモニタリング". doi : 10.1007/978-3-540-30206-3_12 .
↑ Mehrabian, Mohammadreza; Khayatian, Mohammad; Shrivastava, Aviral; Eidson, John C.; Derler, Patricia; Andrade, Hugo A.; Li-Baboud, Ya-Shian; Griffor, Edward; Weiss, Marc; Stanton, Kevin (2017). "サイバーフィジカルシステムのタイミングをテストするためのタイムスタンプ時間論理 (TTL)" . ACM Transactions on Embedded Computing Systems . 16 (5s): 1– 20. doi : 10.1145/3126510 . S2CID 3570088 .
↑ Koymans, R. (1990). "Specifying real-time properties with metric temporal logic", Real-Time Systems 2 (4): 255–299. doi : 10.1007/BF01995674 .
↑リー、シャオ、クリスティアン・ヨアン・ヴァシル、カリン・ベルタ。「時相論理報酬による強化学習」土井：10.1109/IROS.2017.8206234
↑マイケル・R・クラークソン;フィンクバイナー、ベルント。コレイニ、マスード。ミシンスキー、クリストファー K.ラーベ、マーカス N.サンチェス、セザール (2014)。「ハイパープロパティの時間論理」。セキュリティと信頼の原則。コンピューターサイエンスの講義ノート。 Vol. 8414. pp. 265–284 . doi : 10.1007/978-3-642-54792-8_15。ISBN 978-3-642-54791-1. S2CID 8938993 .
↑ Rescher, Nicholas (1968). "位相論理". Topics in Philosophical Logic . pp. 229–249 . doi : 10.1007/978-94-017-3546-9_13 . ISBN 978-90-481-8331-9。
↑フォン・ライト、ゲオルク・ヘンリック（ 1979）。「場所の様相論理」。ニコラス・レッシャーの哲学。65-73頁。doi : 10.1007 / 978-94-009-9407-2_9。ISBN 978-94-009-9409-6。

参考文献

モルデカイ・ベン＝アリ、ゾハル・マンナ、アミール・プヌエリ：「分岐時間の時間論理」POPL 1981: 164–176
アミール・プヌエリ：プログラムの時間論理FOCS 1977: 46–57
Venema, Yde, 2001、「時間論理」、Goble, Lou 編、『The Blackwell Guide to Philosophical Logic』所収。Blackwell。
EA Emerson と Chin-Laung Lei、「モデル検査のための様相：分岐時間論理の逆襲」、Science of Computer Programming 8、pp. 275–306、1987 年。
E.A.エマーソン、「時間論理と様相論理」、理論計算機科学ハンドブック、第16章、MIT出版、1990年
PSLの実践的入門、シンディ・アイスナー、ダナ・フィッシュマン
Vardi, Moshe Y. (2008). 「教会とそれ以前から PSLへ」. Orna Grumberg、Helmut Veith (編) 『モデル検査25年：歴史、成果、展望』所収. Springer. ISBN 978-3-540-69849-4。プレプリント。コンピュータ科学と工学において、一見無関係に見えるアイデアがどのように結びついたのかについての歴史的考察。（本論文のタイトルにあるチャーチという名前は、チャーチがハードウェア検証の方法を提案した、あまり知られていない1957年の論文を指している。）

さらに読む

ピーター・オーストロム、ペル・F・V・ハスレ（1995）。時間論理：古代の思想から人工知能へ。シュプリンガー。ISBN 978-0-7923-3586-3。

外部リンク

スタンフォード哲学百科事典：「時間論理」—アンソニー・ガルトン著。
イデ・ヴェネマによる時間論理学では、構文と意味論の形式的記述、公理化の問題を取り上げています。また、カンプの二項時間演算子（since、until）についても扱っています。
イアン・ホジキンソンによる時間論理におけるゲームに関する注釈（一階述語論理の形式的記述を含む）
CADP – さまざまな時間論理のための汎用モデルチェッカーを提供する
PATは、CSPとその拡張機能（共有変数、配列、幅広い公平性を含む）に対応した、強力な無料のモデルチェッカー、LTLチェッカー、シミュレーター、および改良チェッカーです。

[1] ヴァルディ 2008、153ページ

[v154-2] 1 2 3 Vardi 2008、p. 154

[:0-3] 1 2 Łoś、イェジ（1947）。「ポドスタウィ分析方法論、ミラ」。Zasoby Biblioteki Głównej Umcs (ポーランド語)。ナクウ。 Uniwersytetu Marii Curie-Skłodowskiej。

[:1-4] 1 2 3 Øhrstrøm, Peter (2019). 「近代時間論理の初期の歴史におけるANPriorとJerzy Łośの貢献の意義」 .時間の論理と哲学：Priorからのさらなるテーマ、第2巻. 時間の論理と哲学。ISBN 9788772102658。

[:2-5] 1 2 Rescher, Nicholas; Garson, James (1969 年 1 月). "位相論理" . The Journal of Symbolic Logic . 33 (4): 537– 548. doi : 10.2307/2271360 . ISSN 0022-4812 . JSTOR 2271360 . S2CID 2110963 .

[6] Peter Øhrstrøm; Per FV Hasle (1995). Temporal logic: from ancient ideas to artificial intelligence . Springer. ISBN 978-0-7923-3586-3。176～178ページ、210ページ

[7] 「時間論理（スタンフォード哲学百科事典）」。Plato.stanford.edu 。 2014年7月30日取得。

[CarnielliPizzi2008-8] ウォルター・カルニエリ、クラウディオ・ピッツィ（2008）。『モダリティとマルチモダリティ』。シュプリンガー。181ページ。ISBN 978-1-4020-8589-5。

[TessarisFranconi2009-9] Sergio Tessaris; Enrico Franconi; Thomas Eiter (2009). Reasoning Web. Semantic Technologies for Information Systems: 5th International Summer School 2009, Brixen-Bressanone, Italy, August 30 – September 4, 2009, Tutorial Lectures . Springer. p. 112. ISBN 978-3-642-03753-5。

[Tkaczyk_2019_259–276-10] 1 2トカチク、マルシン。ヤルムジェク、トマシュ (2019)。「Jerzy Łoś 位置微積分学と時間論理の起源」論理と論理哲学。28 (2): 259–276。土井: 10.12775/LLP.2018.013。ISSN 2300-9802。

[11] Prior, Arthur Norman (2003). Time and modality: the John Locke lectures for 1955–6, delivered at the University of Oxford . Oxford: The Clarendon Press. ISBN 9780198241584OCLC 905630146

[12] Lawford, M. (2004). "時間論理入門" (PDF) .マクマスター大学コンピュータサイエンス学部.

[13] ゴランコ、ヴァレンティン; ガルトン、アントニー (2015). 「時間論理」。ザルタ、エドワード N. (編) 『スタンフォード哲学百科事典』（2015 年冬版）。スタンフォード大学形而上学研究室。

[14] ミュラー、トーマス (2011)。「時制または時間論理」(PDF)。レオン・ホルステン編『哲学論理の連続体コンパニオン』A&C Black、329ページ。

[15] バージェス、ジョン・P. (2009).哲学的論理学. プリンストン、ニュージャージー州: プリンストン大学出版局. p. 21. ISBN 9781400830497OCLC 777375659。

[16] バージェス、ジョン・P. (2009).哲学的論理学. プリンストン、ニュージャージー州: プリンストン大学出版局. p. 17. ISBN 9781400830497OCLC 777375659。

[17] 「時間論理」。スタンフォード哲学百科事典。2020年2月7日。 2022年4月19日取得。

[autogenerated2004-18] 1 2 Maler, O.; Nickovic, D. (2004). "連続信号の時間的特性のモニタリング". doi : 10.1007/978-3-540-30206-3_12 .

[19] Mehrabian, Mohammadreza; Khayatian, Mohammad; Shrivastava, Aviral; Eidson, John C.; Derler, Patricia; Andrade, Hugo A.; Li-Baboud, Ya-Shian; Griffor, Edward; Weiss, Marc; Stanton, Kevin (2017). "サイバーフィジカルシステムのタイミングをテストするためのタイムスタンプ時間論理 (TTL)" . ACM Transactions on Embedded Computing Systems . 16 (5s): 1– 20. doi : 10.1145/3126510 . S2CID 3570088 .

[20] Koymans, R. (1990). "Specifying real-time properties with metric temporal logic", Real-Time Systems 2 (4): 255–299. doi : 10.1007/BF01995674 .

[21] リー、シャオ、クリスティアン・ヨアン・ヴァシル、カリン・ベルタ。「時相論理報酬による強化学習」土井：10.1109/IROS.2017.8206234

[22] マイケル・R・クラークソン;フィンクバイナー、ベルント。コレイニ、マスード。ミシンスキー、クリストファー K.ラーベ、マーカス N.サンチェス、セザール (2014)。「ハイパープロパティの時間論理」。セキュリティと信頼の原則。コンピューターサイエンスの講義ノート。 Vol. 8414. pp. 265–284 . doi : 10.1007/978-3-642-54792-8_15。ISBN 978-3-642-54791-1. S2CID 8938993 .

[23] Rescher, Nicholas (1968). "位相論理". Topics in Philosophical Logic . pp. 229–249 . doi : 10.1007/978-94-017-3546-9_13 . ISBN 978-90-481-8331-9。

[24] フォン・ライト、ゲオルク・ヘンリック（ 1979）。「場所の様相論理」。ニコラス・レッシャーの哲学。65-73頁。doi : 10.1007 / 978-94-009-9407-2_9。ISBN 978-94-009-9409-6。

[ 1 ]

[

[

[ 7 ]

[ 8 ]

[ 9 ]

[ 10 ]

[

[ 12 ]

[ 13 ]

[

[ 15 ]

[

[ 17 ]

[ 18 ]

[ 19 ]

[ 20 ]

[ 21 ]

[ 22 ]

[ 23 ]

[ 24 ]

時間論理

モチベーション

歴史

ウォシュの位置論理

構文

オリジナルの公理系

プライアーの時制論理（TL）

構文と意味論

最小限の公理的論理

述語論理への翻訳

時間演算子

時間論理

関連項目

注記

参考文献

さらに読む

外部リンク

関連するトピック

論理学

時間

時間論理は形式検証

アーサー・プライアーによって導入され、