トップQs
タイムライン
チャット
視点

線形時相論理

ウィキペディアから

Remove ads

線形時相論理(せんけいじそうろんり、Linear Temporal Logic、LTL)とは、時間に関する様相を持つ様相時相論理である。LTLでは、ある条件が最終的に真となるとか、別の事実が真になるまでその条件は真であるとかいった将来の出来事について論理式で表すことができる。

文法

LTL では変項 や一般的な論理作用素 の他に以下の時相様相作用素を使用する:

  • N (next)
  • Gglobally)
  • F (in the future)
  • U (until)
  • R (release)

最初の3つの作用素は単項演算である。従って、論理式であれば、N も論理式である。最後の2つの作用素は二項演算である。従って、 が論理式であれば、 U も論理式である。

Remove ads

意味論

要約
視点

LTLの論理式の評価は経路上の位置における逐次的な真理値として評価される。LTLの論理式はその経路上の位置 0 において真であるときのみ真である。様相作用素の意味論は以下のように与えられる。

さらに見る ...

以下の恒等式が成り立つことから、作用素の種類を減らすことができる:

  • F = true U
  • G = false R = F
  • R = ( U )
Remove ads

重要な特性

線形時相論理で表現できる重要な特性として次の2種類がある。安全性特性は「何か悪いことが決して起こらない」ことを意味する(G)。活性特性は「何か良いことがいずれ起きる」ことを意味する(F)。安全性特性とは、有限な期間での反例を無限の時系列に拡張しても反例であるような状態である。一方活性特性は、有限な期間での反例を無限の時系列に拡張したとき、それが反例でなくなる(その論理式が真となる)状態である。

他の論理との関係

線形時相論理(LTL) は CTL* (英語版) の一部である。

LTLは、後者(successor、ペアノの公理参照)と「小なり」の関係についての一階述語論理 FO[S,<] と等価である。また、クリーネスターのない正規表現や loop complexity が 0 であるような決定性有限オートマトンも LTL と等価である。

関連項目

外部リンク

Loading related searches...

Wikiwand - on

Seamless Wikipedia browsing. On steroids.

Remove ads