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