模型检查

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

SharpLogic 不执行智能体，而是对图结构做符号化分析，因而兼具模型检查的穷尽性与属性测试的轻量性。

Dan Klein认为，在系统上叠加第二个模型来检查第一个是弱修复，因为两者都可能出错且往往在相同的困难案例上失败，他估计80%检查80%最终约为82%。