What's important to put those results in context for those who are not familiar with the subject is that, in the context of complexity theory, the "model checking problem" does not refer to the complexity of a particular model checker algorithm, but to the inherent complexity of the problem of deciding whether a program M satisfies some property 𝜑 (i.e. whether M is a model of 𝜑 in the formal logic sense). The "model checking problem" is the closest to a mathematical description of what we usually mean when we talk of "reasoning about a program."
* http://www.lsv.fr/Publis/PAPERS/PDF/Sch-aiml02.pdf
* http://www.lsv.fr/Publis/PAPERS/PDF/DLS-jcss-param.pdf
* https://www.cis.upenn.edu/~alur/Zohar03.pdf
What's important to put those results in context for those who are not familiar with the subject is that, in the context of complexity theory, the "model checking problem" does not refer to the complexity of a particular model checker algorithm, but to the inherent complexity of the problem of deciding whether a program M satisfies some property 𝜑 (i.e. whether M is a model of 𝜑 in the formal logic sense). The "model checking problem" is the closest to a mathematical description of what we usually mean when we talk of "reasoning about a program."
I've summarized these results and more here: https://pron.github.io/posts/correctness-and-complexity