-
题名谓词μ演算和模态图的语义一致性
被引量:3
- 1
-
-
作者
刘剑
林惠民
-
机构
中国科学院软件研究所计算机科学重点实验室
-
出处
《软件学报》
EI
CSCD
北大核心
2003年第10期1672-1680,共9页
-
基金
国家自然科学基金~~
-
文摘
模态图是谓词m演算的一种有效的图形表示形式.证明了谓词m演算和模态图的语义一致性,详细讨论了谓词m演算公式、嵌套谓词等式系和模态图之间的关系,并给出了一种优化的从线性公式到嵌套谓词等式系的转换算法.
-
关键词
不动点
谓词μ演算
嵌套谓词等式系
模态图
-
Keywords
fixed-point
predicate m-calculus
nested predicate equation
modal graph
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
-
题名基于偏序规律的μ-演算一阶谓词界程逻辑模型检测
被引量:4
- 2
-
-
作者
江华
-
机构
闽南师范大学粒计算重点实验室
韶关学院信息科学与工程学院
-
出处
《计算机学报》
EI
CSCD
北大核心
2016年第12期2547-2561,共15页
-
基金
国家自然科学基金(61472406)
福建省自然科学基金(2015J01269
+3 种基金
2016J01304)
韶关市哲学社会科学规划课题(G2012001)
广东省自然科学基金(S2013010015944)
闽南师范大学人才引进项目资助~~
-
文摘
基于μ-演算的一阶谓词界程逻辑,用谓词变量构造不动点公式,方便描述闭环系统的性质,公式语义简洁.该逻辑在有限控制移动界程上的模型检测目前性能最好的算法的时间复杂度与公式中不动点算子交错嵌套深度d呈指数关系,空间复杂度与d呈线性关系.文中设计了一个基于μ-演算的一阶谓词界程逻辑在有限控制移动界程上的模型检测高效算法,这也是目前已知的第3个同类算法,算法的时间复杂度与d/2+1呈指数关系,空间复杂度与d呈线性关系.文中所做的工作有:(1)找到了基于μ-演算的一阶谓词界程逻辑模型检测计算过程中的中间结果满足的两组偏序关系;(2)利用找到的偏序关系设计了一个快速模型检测算法;(3)分析了算法的复杂度.
-
关键词
模型检测
移动界程
μ-演算
嵌套谓词等式系
-
Keywords
model checking
mobile ambient
μ-calculus
nested predicate equations
-
分类号
TP316
[自动化与计算机技术—计算机软件与理论]
-
-
题名移动界程模型检测
被引量:3
- 3
-
-
作者
江华
李祥
-
机构
韶关学院计算机科学学院
中山大学地理科学与规划学院
贵州大学计算机软件与理论研究所
-
出处
《计算机研究与发展》
EI
CSCD
北大核心
2009年第10期1750-1757,共8页
-
文摘
首次将嵌套谓词等式系应用到带递归的谓词界程逻辑模型检测中,提出了第1个时间复杂性与逻辑公式的交错嵌套深度呈指数关系的局部模型检测算法,这也是目前已知的第2个带递归的谓词界程逻辑模型检测算法.所做的工作有:①讨论了谓词界程逻辑公式与嵌套谓词等式系间语义的等价性,给出了谓词界程逻辑公式转换成嵌套谓词等式系的方法;②讨论了谓词界程逻辑模型检测问题,给出了具体算法,并分析了算法的复杂性.
-
关键词
模型检测
移动界程
谓词μ-演算
嵌套谓词等式系
算法复杂性
-
Keywords
model checking
mobile ambient
predicate μ-calculus
nested predicate equations
complicacy of algorithm
-
分类号
TP316
[自动化与计算机技术—计算机软件与理论]
-