-
题名基于决策过程的广义可能性计算树逻辑模型检测
被引量：12
- 1
-
-
作者
马占有
李永明
-
机构
陕西师范大学计算机科学学院
北方民族大学计算机科学与工程学院
-
出处
《中国科学：信息科学》
CSCD
北大核心
2016年第11期1591-1607,共17页
-
基金
国家自然科学基金(批准号:11271237
61228305
+2 种基金
61462001)
高等学校博士学科点专项科研基金(批准号:20130202110001
20130202120002)
-
文摘
本文研究了广义可能性计算树逻辑模型检测算法及其在系统验证中的应用,特别是在非确定性系统验证中的应用.首先引入作为系统模型的广义可能性决策过程和描述系统属性的广义可能性计算树逻辑,然后给出基于广义可能性决策过程的广义可能性计算树逻辑模型检测算法.该算法最大的优点是利用决策过程中的调度,将模型检测问题转换为多项式时间内模糊矩阵的运算或模糊矩阵不动点的计算.最后通过一个实例说明了广义可能性计算树逻辑模型检测在非确定性系统中的应用.
-
关键词
非确定性系统
广义可能性决策过程
调度
广义可能性计算树逻辑
模型检测
-
Keywords
nondeterministic system
generalized possibilistic decision process
scheduler
generalized possibilistic computation tree logic
model checking
-
分类号
TP301.6
[自动化与计算机技术—计算机系统结构]
-
-
题名广义可能性决策过程的计算树逻辑模型检测
被引量：3
- 2
-
-
作者
马占有
李永明
-
机构
陕西师范大学计算机科学学院
北方民族大学计算机科学与工程学院
-
出处
《计算机工程与科学》
CSCD
北大核心
2015年第11期2162-2168,共7页
-
基金
国家自然科学基金资助项目(11271237
61228305
+1 种基金
61462001)
北方民族大学资助项目(2014XB213)
-
文摘
模型检测作为一种形式化验证技术,已被广泛应用于各种并发系统的正确性验证。针对具有非确定性选择和广义可能性分布的并发系统,引入广义可能性决策过程作为此类系统的模型;给出描述其性质的规范语言广义可能性计算树逻辑的概念;研究此类系统的广义可能性计算树逻辑模型检测问题。结论表明,其模型检测算法的时间复杂度也为多项式时间。所获得的结果扩大了广义可能性测度在模型检测中的应用范围。
-
关键词
并发系统
广义可能性决策过程
广义可能性计算树逻辑
模型检测
-
Keywords
concurrent systems
generalized possibilistic decision process
generalized possibilistic computation tree logic （GPCTL）
model checking
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
-
题名具有多值决策过程的广义可能性计算树逻辑模型检测
被引量：1
- 3
-
-
作者
袁申
魏杰林
李永明
-
机构
陕西师范大学计算机科学学院
-
出处
《计算机工程与科学》
CSCD
北大核心
2019年第1期88-97,共10页
-
基金
国家自然科学基金(11671244)
-
文摘
模型检测是一种自动验证软硬件系统行为的有效技术。为了对包含非确定性信息、不一致信息的并发系统进行形式化验证,在可能性理论、多值逻辑的基础上,研究了具有多值决策过程的广义可能性多值计算树逻辑模型检测算法,及其在检验非确定性系统中的具体应用。首先构造了多值决策过程作为系统模型,用多值计算树逻辑描述系统属性。然后给出具有多值决策过程的广义可能性多值计算树逻辑的模型检测算法,该算法将模型检测的具体问题转换为多项式时间内的模糊矩阵运算。最后就包含非确定性选择的多值系统的模型检测问题,给出一个具体的应用实例。
-
关键词
模型检测
多值计算树逻辑
广义可能性测度
多值决策过程
-
Keywords
model checking
multi-valued computation tree logic
generalized possibilistic measure
multi-valued decision process
-
分类号
TP301.2
[自动化与计算机技术—计算机系统结构]
-
