模型检测学习笔记（一）：绪论

一、概念  模型检测是一种用于自动验证有限状态并发系统的技术；模型检测算法通常对系统状态空间进行穷尽搜索来确定性质的真假。如果资源充足，检测过程总是以是或非终止，是表示系统满足性质，否表示不满足性质，并自动给出一个反例。 模型检测中最大的困难是状态空间爆炸；解决状态空间爆炸有如下方法： 符号化模型检验技术； 偏序规约技术； on-the-fly技术； 对称技术； 抽象和组合技术； 二、模型检测的过

>>阅读原文<<