LTL model checking

decidability

finite state system is decidable. But, LTL model checking for infinite state system is undecidable.

automata-theoretic approach

对Kripke Structure K和LTL公式$\varphi$，如果将其都翻译为NBA，可以通过检查$A_K\subseteq A_{\varphi }$解决。但是NBA求补很困难，更佳的方法是检查$A_K\cap A_{\neg \varphi }=\varnothing$（LTL公式的否定容易求）

因为$A_K$所有的状态都是接受的，所以在求交时，只需要算product automaton即可。自动机的大小是$O(|K|\times 2^{|\varphi |})$，这也是这种模型检测方法的复杂度（非空性判定是线性的），实际中主要是K的大小影响效率。

LTL翻译见LTL translation to Büchi automata，Kripke Structure翻译见Kripke Structure to Büchi automata