基于偏序规律的μ-演算一阶谓词界程逻辑模型检测
发布时间：2017-10-05 06:30
本文关键词：基于偏序规律的μ-演算一阶谓词界程逻辑模型检测
更多相关文章： 模型检测 移动界程 μ-演算 嵌套谓词等式系
【摘要】：基于μ-演算的一阶谓词界程逻辑,用谓词变量构造不动点公式,方便描述闭环系统的性质,公式语义简洁.该逻辑在有限控制移动界程上的模型检测目前性能最好的算法的时间复杂度与公式中不动点算子交错嵌套深度d呈指数关系,空间复杂度与d呈线性关系.文中设计了一个基于μ-演算的一阶谓词界程逻辑在有限控制移动界程上的模型检测高效算法,这也是目前已知的第3个同类算法,算法的时间复杂度与d/2+1呈指数关系,空间复杂度与d呈线性关系.文中所做的工作有:(1)找到了基于μ-演算的一阶谓词界程逻辑模型检测计算过程中的中间结果满足的两组偏序关系;(2)利用找到的偏序关系设计了一个快速模型检测算法;(3)分析了算法的复杂度.
【作者单位】： 闽南师范大学粒计算重点实验室;韶关学院信息科学与工程学院;
【关键词】： 模型检测 移动界程 μ-演算 嵌套谓词等式系
【基金】：国家自然科学基金(61472406) 福建省自然科学基金(2015J01269,2016J01304) 韶关市哲学社会科学规划课题(G2012001) 广东省自然科学基金(S2013010015944) 闽南师范大学人才引进项目资助~~
【分类号】：O141.1
【正文快照】： 1引言移动界程演算(Mobile Ambients)[1]最先由Cardelli等人于2000年提出,用于分布式移动计算系统的形式化建模与验证,空间描述能力强.2000年Cardelli等人[2]首次提出界程逻辑,具备同时表达进程在时间和空间上演变的能力.2001年Cardelli等人[3]将受囿名量词和新名量词引入界程
【相似文献】
中国期刊全文数据库 前10条
1 陈清亮;朱可宜;;多智能体协同的认知规范模型检测算法[J];中山大学学报(自然科学版);2009年01期
2 周从华;邢支虎;刘志锋;王昌达;;马尔可夫决策过程的限界模型检测[J];计算机学报;2013年12期
3 吉猛;胡克瑾;;基于模型检测的电子商务鉴证技术[J];陕西师范大学学报(自然科学版);2006年04期
4 宁正元;胡山立;赖贤伟;;交互时态信念逻辑及其模型检测[J];南京大学学报(自然科学版);2008年02期
5 王曦;徐中伟;梅萌;;基于模型检测的软件安全性验证方法[J];武汉大学学报(理学版);2010年02期
6 王晶;张广泉;;基于概率时间自动机的模型检测反例表示研究[J];苏州大学学报(自然科学版);2011年02期
7 高妍妍;李曦;周学海;;L4进程间通信机制的模型检测方法[J];中国科学院研究生院学报;2011年06期
8 王扣武;张s，
本文编号：975290
本文链接：https://www.wllwen.com/shekelunwen/ljx/975290.html
