命题μ-演算全局模型检测的高效算法设计

作     者：江华 Jiang Hua

作者机构：韶关学院计算机科学学院广东韶关512005 

出 版 物：《计算机研究与发展》 (Journal of Computer Research and Development)

年 卷 期：2010年第47卷第8期

页      码：1424-1433页

摘      要：在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问题 不动点 

学科分类：0810[工学-土木类] 0808[工学-自动化类] 0839[0839] 08[工学] 0835[0835] 0811[工学-水利类] 0812[工学-测绘类] 081202[081202] 

核心收录：

馆 藏 号：203441457...