Automata-Based LTL Model Checking

An LTL model-checking algorithm is a decision procedure which for a transition system \(\texttt{TS}\) and LTL formula ϕ returns the answers "yes" if \(\texttt{TS} \models \phi\) and "no" (plus a counterexample) if \(\texttt{TS} \nvDash \phi\). The counterexample consists of an appropriate finite prefix of an infinite path in \(\texttt{TS}\) where ϕ does not hold.