基于动态Kripke语义直接模型检测及其应用分析

在过去的20年里，基于Kdpkc语义结构的模型检测技术在集成电路设计，网络协议分析，程序正确性验证及程序错误发现等方面证明了其有效性和能力．最近，在诸如使用SAT分析工具、有界模型检测等避免OBDDs的模型检测研究方面取得了相当大的进展提出的动态Knpke 语义结构是让原子命题集合AP可以改变．基于这个方法，提出了一个直接模型检测算法