Complexity of Model Checking

Mathematical logic and computational complexity have close connections that can be traced to the roots of computability theory and the classical decision problem. In the context of complexity, some well-known fundamental problems are: satisfiability testing of formulas (in some logic), proof complexity, and the complexity of checking if a given model satisfies a given formula. The Model Checking problem, which is the topic of the present article, is also of practical relevance since efficient model checking algorithms for temporal/modal logics are useful in formal verification. In their excellent and detailed survey, Arne Meier, Martin Mundhenk, Julian-Steffen Müller, and Heribert Vollmer tell us about the complexity of model check-ing for various logics: temporal, modal and hybrid and their many fragments. Their article brings out the intricate structures involved in the reductions and the effectiveness of standard complexity classes in capturing the complexity of model checking