Computation Tree Logic Model Checking for Nondeterminisitc Fuzzy Kripke Structure

FAN Yan-huan; LI Yong-ming; PAN Hai-yu

doi:10.3969/j.issn.0372-2112.2018.01.021

您当前的位置：

首页 >

文章列表页 >

Computation Tree Logic Model Checking for Nondeterminisitc Fuzzy Kripke Structure

更新时间：2025-07-16

- Computation Tree Logic Model Checking for Nondeterminisitc Fuzzy Kripke Structure
- Acta Electronica Sinica Vol. 46, Issue 1, Pages: 152-159(2018)
- 作者机构：
  
  1. 陕西师范大学计算机科学学院,陕西,西安,710062
  2. 青海师范大学民师院数学系,青海,西宁,810008
  3. 泰州学院计算机科学与技术学院,江苏,泰州,225300
  4. 陕西师范大学计算机科学学院,陕西,西安,710062
  5. 青海师范大学民师院数学系,青海,西宁,810008
  6. 泰州学院计算机科学与技术学院,江苏,泰州,225300
- 作者简介：
- 基金信息：
- DOI：10.3969/j.issn.0372-2112.2018.01.021
  CLC： TP301.2
- Published Online：25 January 2018，
  
  Published：2018
- 稿件说明：
移动端阅览
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：

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

Views

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

The Model Checking Problem of Computing Tree Logic Based on Generalized Possibility Measures

Research on Interaction Modeling and Mismatch Checking of Time-Aware Web Services

Exact Acceleration of Real-Time Model Checking Based on Parking Cycle

On the Finite Strong Completeness of NM321;

Specification and Verification of Web Service Composition Based on XYZ/ADL

Related Author

LI Yong-ming

LIANG Chang-jian

Sheng

WANG Sheng

RONG Mei

ZHANG Guang-quan

ZHUANG Lei

WANG Cong-yin

Related Institution

School of Mathematics and Statistics, Shangqiu Normal University

School of Mathematics and Information Science Shaanxi Normal University Xi'an Shaanxi China

School of Mathematics and Statistics Shangqiu Normal University Shangqiu Henan China

School of Mathematics and Information Science, Shaanxi Normal University

Shenzhen Tourism CollegeJinan UniversityShenzhenGuangdong 518053China

⁰