电子学报 ›› 2018, Vol. 46 ›› Issue (1): 152-159.DOI: 10.3969/j.issn.0372-2112.2018.01.021

• 学术论文 • 上一篇    下一篇

不确定型模糊Kripke结构的计算树逻辑模型检测

范艳焕1,2, 李永明1, 潘海玉1,3   

  1. 1. 陕西师范大学计算机科学学院, 陕西西安 710062;
    2. 青海师范大学民师院数学系, 青海西宁 810008;
    3. 泰州学院计算机科学与技术学院, 江苏泰州 225300
  • 收稿日期:2017-05-19 修回日期:2017-08-14 出版日期:2018-01-25
    • 通讯作者:
    • 李永明
    • 作者简介:
    • 范艳焕,女,1987年生于河南商丘.现为陕西师范大学计算机科学学院博士研究生.主要研究方向为定量模型检测.E-mail:fan.fan1222@163.com
    • 基金资助:
    • 国家自然科学基金 (No.11671244,No.61261047,No.61672023,No.61673352); 教育部博士点基金 (No.20130202110001); 青海省自然科学基金 (No.2014-ZJ-908); 江苏高校"青蓝工程"

Computation Tree Logic Model Checking for Nondeterminisitc Fuzzy Kripke Structure

FAN Yan-huan1,2, LI Yong-ming1, PAN Hai-yu1,3   

  1. 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
  • Received:2017-05-19 Revised:2017-08-14 Online:2018-01-25 Published:2018-01-25
    • Supported by:
    • National Natural Science Foundation of China (No.11671244, No.61261047, No.61672023, No.61673352); Ph.D. Programs Foundation of Ministry of Education of China (No.20130202110001); Natural Science Foundation of Qinghai Province (No.2014-ZJ-908); Blue Project in Jiangsu Province

摘要: 本文研究了不确定型模糊Kripke结构的计算树逻辑的模型检测问题,并说明了该问题可以在对数多形式时间内解决.首先给出了不确定型模糊Kripke结构的定义,引入了模糊计算树逻辑的语法和语义.为了刻画存在量词∃和任意量词∀在不确定型模糊Kripke结构中的两种语义解释,在模糊计算树逻辑语法中引入了路径量词∃sup,∃inf和∀sup,∀inf,分别用于替换存在量词∃和任意量词∀.其次讨论了基于不确定型模糊Kripke结构的计算树逻辑模型检测算法,特别地对于模糊计算树逻辑公式∃suppUq,∀suppUq,∃infpUq和∀infpUq分别给出时间复杂度为对数多项式时间的改进算法.

关键词: 模型检测, 计算树逻辑, 模糊逻辑, Kripke结构, 时态逻辑

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.

Key words: model checking, computation tree logic, fuzzy logic, Kripke structure, temporal logic

中图分类号: