首页 | 本学科首页   官方微博 | 高级检索  
     

命题μ-演算全局模型检测的高效算法设计
引用本文:江华.命题μ-演算全局模型检测的高效算法设计[J].计算机研究与发展,2010,47(8).
作者姓名:江华
作者单位:韶关学院计算机科学学院,广东韶关,512005
摘    要:在Long, Browne, Jha 和 Marrero等人工作的基础上,详细分析了用Tarski不动点定理计算不动点交替嵌套深度为4的命题μ-演算公式的计算过程,找到了计算中间结果间具有的两组偏序关系,利用这两组偏序关系设计了一个高效的命题μ-演算全局模型检测算法,该算法与Long等人提出的算法有相似的时间复杂度(O((2n+1)- d/2 - +1)相对于O(n- d/2 - +1)),但空间复杂度有很大的改进(O(dn)相对于O(n- d/2 - +1)),其中n是变迁系统的状态规模,d是命题μ-演算公式中不动点算子的嵌套深度.算法性能的改进对于命题μ-演算模型检测技术的理论研究与实际推广应用都意义重大.

关 键 词:模型检测  μ-演算  计算复杂度  NP∩co-NP问题  不动点
本文献已被 万方数据 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号