TL;DR
「ある性質が常に成り立つ」「ある性質がいつか成り立つ」といった、時間的な要素を含む論理体系。
なぜ必要か
システムのハードウェアやソフトウェアが要求仕様を満たすことを確かめるために、形式手法で使われる。
仕組み
Wikipedia によると、時相論理では次のような時相演算子を使う。X（Next）は次の状態で成り立つこと、F（Finally）は将来のいずれかの時点で成り立つこと、G（Globally）は今後ずっと成り立つこと、U（Until）は ψ が成り立つまで φ が成り立ち続けることを表す。
時間を一本の系列とみなす線形時相論理（LTL）と、分岐する未来を扱う計算木論理（CTL）がある。CTL では A（すべての経路）と E（ある経路）で経路の範囲を指定する。アーサー・プライアーが 1950 年代に提唱し、計算機科学ではアミール・プヌーリが LTL を、クラークとエマーソンが CTL を発展させた。
例
「要求が発生したら、最終的には必ずアクセスが承認される」のような要求仕様を厳密に書ける。こうした性質をモデル検査で確かめる。