| 不确定型模糊Kripke结构的计算树逻辑模型检测 |
| |
| 引用本文： | 范艳焕,李永明,潘海玉.不确定型模糊Kripke结构的计算树逻辑模型检测[J].电子学报,2018,46(1):152-159. |
| |
| 作者姓名： | 范艳焕 李永明 潘海玉 |
| |
| 作者单位： | 1. 陕西师范大学计算机科学学院, 陕西西安 710062;
2. 青海师范大学民师院数学系, 青海西宁 810008;
3. 泰州学院计算机科学与技术学院, 江苏泰州 225300 |
| |
| 摘 要： | 本文研究了不确定型模糊Kripke结构的计算树逻辑的模型检测问题，并说明了该问题可以在对数多形式时间内解决.首先给出了不确定型模糊Kripke结构的定义，引入了模糊计算树逻辑的语法和语义.为了刻画存在量词?和任意量词?在不确定型模糊Kripke结构中的两种语义解释，在模糊计算树逻辑语法中引入了路径量词?sup，?inf和?sup，?inf，分别用于替换存在量词?和任意量词?.其次讨论了基于不确定型模糊Kripke结构的计算树逻辑模型检测算法，特别地对于模糊计算树逻辑公式?suppUq，?suppUq，?infpUq和?infpUq分别给出时间复杂度为对数多项式时间的改进算法.
|
| 关 键 词： | 模型检测 计算树逻辑 模糊逻辑 Kripke结构 时态逻辑 |
| 收稿时间： | 2017-05-19 |
Computation Tree Logic Model Checking for Nondeterminisitc Fuzzy Kripke Structure |
| |
| FAN Yan-huan,LI Yong-ming,PAN Hai-yu.Computation Tree Logic Model Checking for Nondeterminisitc Fuzzy Kripke Structure[J].Acta Electronica Sinica,2018,46(1):152-159. |
| |
| Authors: | FAN Yan-huan LI Yong-ming PAN Hai-yu |
| |
| Affiliation: | 1. College of Computer Science, Shaanxi Normal University, Xi'an, Shaanxi 710062, China;
2. Department of Mathematics in National Normal College, Qinghai Normal University, Xining, Qinghai 810008, China;
3. College of Computer Science and Technology, Taizhou University, Taizhou, Jiangsu 225300, China |
| |
| Abstract: | This paper studys model-checking problem for FCTL (fuzzy computation tree logic) over nondeterministic fuzzy system and shows that it can be solved in linear-logarithmic running time in the size of the system.Firstly,we introduce NFKS (nondeterministic fuzzy kripke structure) which is adapted to model nondeterministic fuzzy system.The syntax and semantics of fuzzy computation tree logic over NFKS are presented.For describing two kinds of semantic explanation,we use path quantifiers ?sup,?inf and ?sup,?inf as substitutes for an existential path quantifier ? and a universal path quantifier ? in the syntax of the CTL.Then,we study the model checking algorithm for fuzzy computation tree logic over NFKS.Furthermore,the improvement algorithms for FCTL formuleas ?suppUq,?suppUq,?infpUq and ?infpUq are given,whose time complexities are linear-logarithmic running time in the size of the system. |
| |
| Keywords: | model checking computation tree logic fuzzy logic Kripke structure temporal logic |
|
| 点击此处可从《电子学报》浏览原始摘要信息 |
|
点击此处可从《电子学报》下载全文 |
|
