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

范艳焕; 李永明; 潘海玉

doi:10.3969/j.issn.0372-2112.2018.01.021

您当前的位置：

首页 >

文章列表页 >

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

学术论文 | 更新时间：2025-07-16

- 不确定型模糊Kripke结构的计算树逻辑模型检测
- Computation Tree Logic Model Checking for Nondeterminisitc Fuzzy Kripke Structure
- 电子学报 2018年46卷第1期页码：152-159
- 作者机构：
  
  1. 陕西师范大学计算机科学学院,陕西,西安,710062
  2. 青海师范大学民师院数学系,青海,西宁,810008
  3. 泰州学院计算机科学与技术学院,江苏,泰州,225300
  4. 陕西师范大学计算机科学学院,陕西,西安,710062
  5. 青海师范大学民师院数学系,青海,西宁,810008
  6. 泰州学院计算机科学与技术学院,江苏,泰州,225300
- 作者简介：
- 基金信息：
  
  国家自然科学基金 (No.11671244，No.61261047，No.61672023，No.61673352）;教育部博士点基金 (No.20130202110001）;青海省自然科学基金 (No.2014-ZJ-908）;江苏高校"青蓝工程"
- DOI：10.3969/j.issn.0372-2112.2018.01.021
  中图分类号： TP301.2
- 网络出版：2018-01-25，
  
  纸质出版：2018
- 稿件说明：
移动端阅览
范艳焕, 李永明, 潘海玉. 不确定型模糊Kripke结构的计算树逻辑模型检测[J]. 电子学报, 2018,46(1):152-159.

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.
范艳焕, 李永明, 潘海玉. 不确定型模糊Kripke结构的计算树逻辑模型检测[J]. 电子学报, 2018,46(1):152-159. DOI： 10.3969/j.issn.0372-2112.2018.01.021.

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. DOI： 10.3969/j.issn.0372-2112.2018.01.021.

摘要

本文研究了不确定型模糊Kripke结构的计算树逻辑的模型检测问题，并说明了该问题可以在对数多形式时间内解决.首先给出了不确定型模糊Kripke结构的定义，引入了模糊计算树逻辑的语法和语义.为了刻画存在量词和任意量词在不确定型模糊Kripke结构中的两种语义解释，在模糊计算树逻辑语法中引入了路径量词

sup

，

inf

和

sup

，

inf

，分别用于替换存在量词和任意量词.其次讨论了基于不确定型模糊Kripke结构的计算树逻辑模型检测算法，特别地对于模糊计算树逻辑公式

sup

，

sup

，

inf

和

inf

分别给出时间复杂度为对数多项式时间的改进算法.

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 s

ubstitutes 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 ∃

sup

∀

sup

∃

inf

and ∀

inf

are given

whose time complexities are linear-logarithmic running time in the size of the system.

关键词

Keywords

references

浏览量

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

广义可能性计算树逻辑的模型检测问题

时间感知Web服务交互行为建模与失配检测方法研究

实时模型检测中基于驻留环的精确加速

NM321;系统的有限强完备性

基于XYZ/ADL的Web服务组合描述与验证