Temporal logic in finite-state verification とは

有限状態検証では、モデルチェッカーは、設計上のエラーを探している並行ソフトウェアシステムを表す有限状態マシンを検査します。エラーは、システムのプロパティとして表現された要件の違反として定義されます。有限状態マシンがプロパティを満たさない場合、モデルチェッカは、場合によっては反例を生成することができます。これは、エラーの発生状況を示すシステムの実行です。
プロパティの仕様は、しばしばリニア・テンポラル・ロジック(LTL)式として記述されます。要件がLTL式として表現されると、モデルチェッカーはモデルに対してこのプロパティを自動的に検証できます。