μ-演算嵌套不动点表达式分块计算算法

doi:10.3969/j.issn.1000-3428.2008.02.002

计算机工程 ›› 2008, Vol. 34 ›› Issue (2): 4-7. doi: 10.3969/j.issn.1000-3428.2008.02.002

μ-演算嵌套不动点表达式分块计算算法

江华1, 2，谭新星2，李祥1

(1. 贵州大学计算机理论与软件研究所，贵阳 550025；2. 广东韶关学院计算机系，韶关 512005)

收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:2008-01-20 发布日期:2008-01-20

Blocked Calculation Algorithm with Nesting Fixed-point Expression for μ-calculus

JIANG Hua1, 2, TAN Xinxing2, LI Xiang1

(1. Institute of Computer Theory and Software, Guizhou University, Guiyang 550025; 2. Computer Department, Shaoguan University, Shaoguan 512005)

Received:1900-01-01 Revised:1900-01-01 Online:2008-01-20 Published:2008-01-20

摘要/Abstract

摘要： 利用叠代计算μ-演算公式时的单调特性，提出了一个分块计算嵌套μ-演算公式的全局算法，算法时间复杂度为，空间复杂度为。由于算法的空间复杂度低，使得不动点算子嵌套深度很大的μ-演算公式的求解成为可能，这在模型检测方面有着非常重要的意义。

关键词: 模型检测, μ-演算, 计算复杂度, NP co-NP问题

Abstract:

This paper puts forward a blocked calculation algorithm for the nesting μ-calculus formula by using the monotonicity of the iterate calculation of the μ-calculus formula, whose time complexity is and space complexity is . For the lower space complexity of the algorithm, it is possible to solve the μ-calculus formula whose fixed-point operator is deep nesting, which is significant in the model checking.

Key words: model checking, μ-calculus, calculation complexity, NP co-NP problem

中图分类号:

TP311

江华; ;谭新星;李祥. μ-演算嵌套不动点表达式分块计算算法[J]. 计算机工程, 2008, 34(2): 4-7.

JIANG Hua; ; TAN Xinxing; LI Xiang. Blocked Calculation Algorithm with Nesting Fixed-point Expression for μ-calculus[J]. Computer Engineering, 2008, 34(2): 4-7.

http://www.ecice06.com/CN/Y2008/V34/I2/4

[1]	谢娜, 谭文安, 曹彦, 赵璐. 移动边缘计算中安全信息流建模与分析[J]. 计算机工程, 2022, 48(5): 35-42,52.
[2]	汪晗,王坤,路文进,汪磊. 无线传感器网络的锚节点优化布设算法[J]. 计算机工程, 2018, 44(8): 105-111.
[3]	张盛峰,汪仟,黄胜,肖傲. HEVC帧间预测编码单元深度快速选择算法[J]. 计算机工程, 2018, 44(10): 258-263.
[4]	王正,许德武,韩建民,鲁剑锋. 一种高阶权限指派约束的安全性与一致性验证[J]. 计算机工程, 2018, 44(1): 171-175,181.
[5]	任胜兵,张健威,吴斌,王志健. Spark环境下基于SMT的分布式限界模型检测[J]. 计算机工程, 2017, 43(6): 19-23,29.
[6]	杨小东,李亚楠,周其旭,高国娟,王彩芬. 基于身份的服务器辅助验证代理重签名方案[J]. 计算机工程, 2017, 43(4): 166-170,176.
[7]	郑先侠,王海泉,李飞,营梦云,周玫君. 大规模天线系统中低复杂度的解码方法研究[J]. 计算机工程, 2017, 43(10): 31-37.
[8]	魏巍,吴孔平,郭来功,秦蒙. 基于联合非负字典学习的遥感图像超分辨重建[J]. 计算机工程, 2016, 42(8): 271-276.
[9]	唐郑熠,王金水,何栋炜,薛醒思,胡文瑜. 馈线自动化算法的形式化建模与验证[J]. 计算机工程, 2016, 42(3): 89-93.
[10]	范馨月,苏艳涛,周非. 一种低复杂度稀疏信道估计算法[J]. 计算机工程, 2016, 42(11): 120-124,130.
[11]	彭新东,杨勇,宋娟萍,蒋芸. 毕达哥拉斯模糊软集及其应用[J]. 计算机工程, 2015, 41(7): 224-229.
[12]	赵璐,张健沛,杨静. 收缩候选回溯集的有状态动态偏序归约方法[J]. 计算机工程, 2015, 41(5): 70-76.
[13]	许兴旺,骆翔宇. 基于MAS 模型检测与抽象的Web 服务验证[J]. 计算机工程, 2015, 41(3): 26-31,36.
[14]	劳佳琪,文中华,伍小辉,唐杰. 一种快速求强规划解的算法[J]. 计算机工程, 2015, 41(3): 162-166.
[15]	伍小辉,文中华,李洋,劳佳琪. 不确定规划中的多Agent带权值强规化算法[J]. 计算机工程, 2015, 41(1): 190-195.

选择文件类型/文献管理软件名称

选择包含的内容

μ-演算嵌套不动点表达式分块计算算法

Blocked Calculation Algorithm with Nesting Fixed-point Expression for μ-calculus

PDF

可视化

被引次数

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

本文评价

模态框（Modal）标题

选择文件类型/文献管理软件名称

选择包含的内容

μ-演算嵌套不动点表达式分块计算算法

Blocked Calculation Algorithm with Nesting Fixed-point Expression for μ-calculus

PDF

可视化

被引次数

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

本文评价