Model checking

Remarks

For CTL the problem can be solved in time $O(\abs{M} \cdot \abs{\varphi})$, where $\abs{M} = \abs{S} + \abs{R}$. The algorithm labels the states with the subformulas of $\varphi$ that they satisfy, from the innermost subformula outward. For LTL the problem is PSPACE-complete in the size of $\varphi$, and it can be solved in time $O(\abs{M} \cdot 2^{O(\abs{\varphi})})$ through a Büchi automaton for $\neg\varphi$.

Example: let $S = \set{s, t}$, $R = \set{(s, t), (t, s)}$, $L(s) = \set{p}$ and $L(t) = \emptyset$. The only path from $s$ is $s\,t\,s\,t \cdots$, so $M, s \models G F p$ in LTL, while $M, s \not\models G p$, since $p \notin L(t)$.

An input with an infinite state set is not an instance of this problem as defined here; for such systems the question can be undecidable.