Counterexamples and Witnesses
A major strength of Model Checking is the possibility of generating a counterexample in case a formula is refuted. (…). In the case of LTL, a counterexample for \(\texttt{TS} \models \phi\) is a sufficiently long prefix of a path π that indicates why π refutes ϕ. For instance, a counterexample for the LTL formula \(\Diamond\) a is a finite prefix of just ¬a-states that ends with a single cycle traversal. Such counterexample suggests that there is a ¬a-path. Similarly, a counterexample for a consists of a path π for which π[1] violates a.
(…)
For CTL the situation is somewhat more involved due to the existential path quantification. For CTL formulae of the form \(\forall \phi\) a sufficiently long prefix of π with \(\pi \models \phi\) provides - as in LTL—sufficient information about the source of the refutation.