時相論理とは？

じそうろんり

「いつか（F）」「常に（G）」「次の時点で（X）」などの時間的演算子を含む論理体系です。

時相論理（temporal logic）は「F φ（いつか φ が真になる）」「G φ（常に φ が真である）」「X φ（次の状態で φ が真）」「φ U ψ（ψ が成り立つまで φ が成り立つ）」などの時間的演算子を持つ様相論理の一種である。プログラムの仕様記述や検証（モデル検査）に広く利用され、LTL（線形時相論理）と CTL（計算木論理）が代表的な体系として知られる。