Loading AI tools
ウィキペディアから
線形時相論理(せんけいじそうろんり、Linear Temporal Logic、LTL)とは、時間に関する様相を持つ様相時相論理である。LTLでは、ある条件が最終的に真となるとか、別の事実が真になるまでその条件は真であるとかいった将来の出来事について論理式で表すことができる。
LTL では変項 や一般的な論理作用素 の他に以下の時相様相作用素を使用する:
最初の3つの作用素は単項演算である。従って、 が論理式であれば、N も論理式である。最後の2つの作用素は二項演算である。従って、 と が論理式であれば、 U も論理式である。
LTLの論理式の評価は経路上の位置における逐次的な真理値として評価される。LTLの論理式はその経路上の位置 0 において真であるときのみ真である。様相作用素の意味論は以下のように与えられる。
以下の恒等式が成り立つことから、作用素の種類を減らすことができる:
線形時相論理で表現できる重要な特性として次の2種類がある。安全性特性は「何か悪いことが決して起こらない」ことを意味する(G)。活性特性は「何か良いことがいずれ起きる」ことを意味する(F)。安全性特性とは、有限な期間での反例を無限の時系列に拡張しても反例であるような状態である。一方活性特性は、有限な期間での反例を無限の時系列に拡張したとき、それが反例でなくなる(その論理式が真となる)状態である。
線形時相論理(LTL) は CTL* (英語版) の一部である。
LTLは、後者(successor、ペアノの公理参照)と「小なり」の関係についての一階述語論理 FO[S,<] と等価である。また、クリーネスターのない正規表現や loop complexity が 0 であるような決定性有限オートマトンも LTL と等価である。
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.