移动界程模型检测
Model Checking for Mobile Ambients作者机构:韶关学院计算机科学学院广东韶关512005 中山大学地理科学与规划学院广州510275 贵州大学计算机软件与理论研究所贵阳550025
出 版 物:《计算机研究与发展》 (Journal of Computer Research and Development)
年 卷 期:2009年第46卷第10期
页 面:1750-1757页
核心收录:
学科分类:08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术(可授工学、理学学位)]
主 题:模型检测 移动界程 谓词μ-演算 嵌套谓词等式系 算法复杂性
摘 要:首次将嵌套谓词等式系应用到带递归的谓词界程逻辑模型检测中,提出了第1个时间复杂性与逻辑公式的交错嵌套深度呈指数关系的局部模型检测算法,这也是目前已知的第2个带递归的谓词界程逻辑模型检测算法.所做的工作有:①讨论了谓词界程逻辑公式与嵌套谓词等式系间语义的等价性,给出了谓词界程逻辑公式转换成嵌套谓词等式系的方法;②讨论了谓词界程逻辑模型检测问题,给出了具体算法,并分析了算法的复杂性.