模型检查（model checking）是一种自动化的形式化验证技术：先为系统建立有限状态模型，再用算法穷举或符号化搜索状态空间，检验是否满足给定的时序逻辑属性；要么给出属性成立的证明，要么返回一条具体的反例路径。