²The original formulation of the model checking problem was: Given a Kripke structure M and a temporal formula f, check whether f is true in M, i.e. whether M is a model for f.