-
题名基于完备抽象解释的性质强保留抽象研究
被引量:1
- 1
-
-
作者
钱俊彦
赵岭忠
蔡国永
-
机构
武汉大学软件工程国家重点实验室
桂林电子科技大学广西可信软件重点实验室
-
出处
《计算机学报》
EI
CSCD
北大核心
2014年第8期1754-1767,共14页
-
基金
国家自然科学基金(61063002
61100186
+6 种基金
61262008)
中国博士后基金(20090450211)
广西自然科学基金(2011GXNSFA018164
2011GXNSFA018166
2012GXNSFAA053220)
武汉大学软件工程国家重点实验室开放基金(SKLSE2010-08-06)
广西壮族自治区教育厅重点项目基金资助~~
-
文摘
在模型检验中,抽象是解决状态空间爆炸问题的重要方法.通常的抽象是非强保留的,即可能存在时序性质在抽象模型不满足而在具体模型满足的情况.文中首先系统地构造μ-演算Lμ语义模型的安全抽象,在此基础上,转换为通用Kripke结构下的安全抽象.然后基于抽象解释框架及完备抽象解释和性质强保留之间的关系,构造使得Lμ性质强保留的最小抽象模型精化,并转换为抽象解释中抽象域的最小完备精化.依据此完备抽象域求得性质强保留的最优抽象状态划分,从而构造出性质强保留且最优的抽象状态转换系统.
-
关键词
抽象解释
模型检验
性质强保留
完备性
精化
-
Keywords
abstract interpretation
model checking
strong preservation
completeness
refinement
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
-
题名一种基于强特征点保留的三维点云数据精简算法
被引量:3
- 2
-
-
作者
郭家富
石磊
严利民
-
机构
上海大学微电子研究与开发中心
-
出处
《工业控制计算机》
2020年第11期92-93,共2页
-
基金
国家自然科学基金,批准号61674100。
-
文摘
介绍了一种改进的三维点云数据精简算法,该算法使用了一种基于强特征点保留的方法,先提取出强特征点数据,再对原始点云进行精简,从而达到点云数据精简的效果。该算法相对于其他算法,在点云数据精简的精度和简度方面都有较大提升。
-
关键词
三维点云
数据精简
强特征点保留
-
Keywords
three-dimensional point cloud
data reduction
strong feature point retention
-
分类号
TP391.41
[自动化与计算机技术—计算机应用技术]
-
-
题名基于完备抽象解释的模型检验CTL公式研究
被引量:5
- 3
-
-
作者
钱俊彦
徐宝文
-
机构
桂林电子科技大学计算机与控制学院
南京大学计算机软件新技术国家重点实验室
南京大学计算机科学与技术系
-
出处
《计算机学报》
EI
CSCD
北大核心
2009年第5期992-1001,共10页
-
基金
国家杰出青年科学基金(60425206)
国家自然科学基金重大研究计划(90818027)
+2 种基金
重点项目(60633010)
国家自然科学基金(60663005)
国家"八六三"高技术研究发展计划目标导向类项目(2009AA01Z147)资助~~
-
文摘
在模型检验中,抽象是解决状态空间爆炸问题的重要方法之一.给定具体Kripke结构和时序描述语言CTL,基于抽象解释框架以及完备抽象解释和性质强保留之间的关系,抽象模型最小精化使得CTL性质强保留,可转换为抽象解释中抽象域的最小完备精化,并且总是存在抽象域的最小完备精化.根据状态标签函数确定初始抽象域,然后通过不动点求解,获得对CTL标准算子完备的最小抽象域,并依据此抽象域求得CTL性质强保留的最优抽象状态划分,最后构造出CTL性质强保留且最优的抽象状态转换系统.并指出了抽象域对CTL标准算子是完备的当且仅当抽象域对补集和标准前向转换是完备的.
-
关键词
抽象解释
抽象模型检验
强保留
完备性
精化
-
Keywords
abstract interpretation
abstract model checking
strong preservation
completeness refinement
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-