Descriptive complexity theory provides a convenient and intuitive way to model a large variety of computational problems. The basic problem studied in descriptive complexity is of the following form: Given a finite relational structure A and a sentence Φ of some logic L, decide ifΦ is satisfied by A. We call this problem the model-checking problem for L. The model-checking problem and variants of it appear in different areas of computer science: The name model-checking is usually associated with automated verification. Here state spaces of finite state systems are modeled by Kripke structures and specifications are formulated in modal or temporal logics. Then checking whether the system has the specified property means checking whether the Kripke structure satisfies the specification, that is, model-checking. In recent years, this approach has very successfully been applied to the verification circuits and protocols.
展开▼
