線形時相論理 線形時相論理の概要

ウィキペディア

線形時相論理

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2020/07/26 19:31 UTC 版)

文法

LTL では変項 $p_{1},p_{2},...$ G $\phi$ F $\phi$ 二項演算 $\psi$ $\psi$

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

• F $\phi$ = true U $\phi$
• G $\phi$ = false R $\phi$ = $\neg$ F $\neg$$\phi$
• $\psi$ R $\phi$ = $\neg$($\neg$$\psi$ U $\neg$$\phi$)

重要な特性

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