Model Checking is an automatic technique for verifying finite-state reactive systems. It is indeed a problem that roots in the model theory: when given both the structure A and a logical formula psi, to decide whether A |= psi. In model checking technique, hard-ware and software systems are represented by their corresponding finite transition systems, and specifications are formulated in some logical framework. The logics chosen for specification are usually modal or temporal logics, like CTL, CTL, etc. But currently some researchers turn back to some classical frameworks, which are extensions of first order logic, mostly the transitive closure logic. The study of descriptive complexity theory shows that in general, the logical framework determines the computational complexity of decision algorithm. So when we fix the logics for model checking, we also get a uniform upper bound of the computational complexity of the checking algorithm.
展开▼
