可能LTL模型检测的两种方法-陕西师范大学学报期刊社网站

陕西师范大学学报（自然科学版）

数学与计算机科学

可能LTL模型检测的两种方法

PDF下载 ()

李永明

(陕西师范大学计算机科学学院，陕西西安 710119)

李永明，男，教授，博士研究生导师，研究方向为模糊系统分析、非经典计算理论.E-mail:liyongm@snnu.edu.cn

摘要:

引入了基于广义可能性测度LTL模型检测的基于路径和基于语言的两种语义,证明了其等价性. 基于可能LTL公式语言等价的方法, 给出基于广义可能性测度的LTL模型检测的算法和复杂性分析.

关键词：

模型检测; 可能性理论; 线性时序逻辑; 语义; 算法

收稿日期：

2014-09-16

中图分类号：

TP301.2

文献标识码：

文章编号：

1672-4291(2014)06-0021-05

基金项目：

国家自然科学基金资助项目(11271237, 61228305); 教育部高等学校博士点基金资助项目(201307180001)

Doi:

Two methods for possibilistic linear temporal logic model checking

LI Yongming

(School of Computer Science, Shaanxi Normal University, Xi′an 710119, Shaanxi, China)

Abstract:

Based on generalized possibility measures, the path semantics and the language semantics of possibilistic LTL model checking are introduced. It is shown that the path semantics and the language semantics of possibilistic LTL model checking are equivalent. Using the equivalence of possibilistic LTL formulae based on the language semantics,the possibilistic LTL model checking and its complexity are presented.

KeyWords:

model checking; possibility theory; linear temporal logic; semantics; algorithm