作者：喻超 毋国庆模型检测形式化验证归约
摘要：限界模型检测主要对路径上的属性进行检测，基于此给出一种编码方法，将LTL公式在路径上展开，从而将限界模型检测转换为命题逻辑的可满足性问题，使用SAT求解工具来完成模型检测过程。阐述归约过程的正确性与完全性，通过一个具体例子证明了该方法的有效性。
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
《计算机工程》（CN：31-1289/TP）是一本有较高学术价值的大型月刊，自创刊以来，选题新奇而不失报道广度，服务大众而不失理论高度。颇受业界和广大读者的关注和好评。 《计算机工程》特点：以最快的速度、科学求实的精神，精选刊登代表计算机行业前沿科研、技术、工程方面的高、精、尖优秀论文。
部级期刊
人气 246641 评论 65
省级期刊
人气 233313 评论 71
人气 227434 评论 35
统计源期刊
人气 210980 评论 73
