模型检测 model checking
模型检测问题是给定模型K与逻辑表达式，判定。最经典的模型检测算法中，模型由Kripke Structure表示，采用某种时序逻辑描述规范。
Handbook of Model checking p 23
In its basic classical form, model checking consists of the following insights:
Modeling. Finite state-transition graphs provide an adequate formalism for the description of finite-state systems such as hardware, but also for finite-state abstractions of software and of communication protocols.
Specification. Temporal logics provide a natural framework for the description of correctness properties for state-transition systems.
Algorithms. There are decision procedures for determining whether a finite state-transition structure is a model of a temporal-logic formula. Moreover, the decision procedures can produce diagnostic counterexamples when the formula is not true in the structure.
模型检测研究的两个主要问题是：
- 设计可扩展的检测算法，用以解决状态爆炸问题。
- 在Kripke和Temporal Logic之外，选取合适的模型和规范的表示方式