Model Checking of Fuzzy Linear Temporal Logic Based on Generalized Possibility Measures

LIANG Chang-jian; LI Yong-ming

doi:10.3969/j.issn.0372-2112.2017.12.020

您当前的位置：

首页 >

文章列表页 >

Model Checking of Fuzzy Linear Temporal Logic Based on Generalized Possibility Measures

更新时间：2025-07-16

- Model Checking of Fuzzy Linear Temporal Logic Based on Generalized Possibility Measures
- Acta Electronica Sinica Vol. 45, Issue 12, Pages: 2971-2977(2017)
- 作者机构：
  
  1. 陕西师范大学数学与信息科学学院,陕西,西安,710119
  2. 商丘师范学院数学与统计学院,河南,商丘,476000
  3. 陕西师范大学数学与信息科学学院,陕西,西安,710119
  4. 商丘师范学院数学与统计学院,河南,商丘,476000
- 作者简介：
- 基金信息：
  
  National Natural Science Foundation of China (No.11271237, No.11671244, No.11401363, No.11501345);Research Fund for the Doctoral Program of Higher Education of China (No.20130202110001)
- DOI：10.3969/j.issn.0372-2112.2017.12.020
  CLC： TP301.2
- Published Online：25 December 2017，
  
  Published：2017
- 稿件说明：
移动端阅览
LIANG Chang-jian, LI Yong-ming. Model Checking of Fuzzy Linear Temporal Logic Based on Generalized Possibility Measures[J]. Acta Electronica Sinica, 2017, 45(12): 2971-2977.
DOI：

LIANG Chang-jian, LI Yong-ming. Model Checking of Fuzzy Linear Temporal Logic Based on Generalized Possibility Measures[J]. Acta Electronica Sinica, 2017, 45(12): 2971-2977. DOI： 10.3969/j.issn.0372-2112.2017.12.020.

摘要

本文首先定义了具有模糊时态的广义可能性线性时序逻辑GPoFLTL（Generalized Possibilistic Fuzzy Linear Tempora Logic）的语构以及基于路径和基于语言的两种语义解释，证明了GPoFLTL在模糊时态方面对GPoLTL（Generalized Possibilistic Linear Tempora Logic）进行了扩张，并通过实例说明了GPoFLTL比GPoLTL具有更强的表达能力；其次在广义可能性测度下通过模糊矩阵运算讨论了不久，几乎总是等几类模糊时态性质的模型检测问题；最后研究了模糊时态性质的必要性阈值模型检测问题，给出了基于自动机的GPoFLTL的阈值模型检测算法及算法的复杂度.

Abstract

In this paper

firstly

the syntax and semantics of GPoFLTL(Generalized Possibilistic Fuzzy Linear Tempora Logic)are given

especially

both the path and language semantics of GPoFLTL are discussed.It is shown that GPoFLTL is the extension to GPoLTL(Generalized Possibilistic Linear Tempora Logic) with respect to fuzzy time

and that GPoFLTL has the stronger expression power than GPoLTL illustrated by some examples.Secondly

GPoFLTL model checking based on the generalized possibility measures is discussed using fuzzy matrix operator

which includes some fuzzy time temporal

Soon

Nearly always

etc.Finally

the necessity threshold model checking problem of fuzzy linear time properties with fuzzy time temporal is studied; furthermore

the algorithm of the necessity threshold model checking of GPoFLTL based on automata method is given

and the time complexity of this method is proved.

关键词

Keywords

references

Views

190

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

A Low Time Complexity Segment Routing Approach for Multi-Commodity Traffic Flow in Mega LEO Constellation

Research on PPI Network Construction and Complex Mining Algorithm Based on Dynamic Graph

Model Checking on Clock Domain Crossing Design of System-on-Chip

A Corrigendum to the Time Complexity of Multicast Routing Algorithm MPH

Unsupervised Salient Object Extraction Based on Sparse Representation

Related Author

LIU Huan

WANG Ning-yuan

LIU Liang

CHEN Dong

HAO Shi-guang

MIN Hui

LUO Ai-jing

LI Peng

Related Institution

Peng Cheng Laboratory

Beijing Institute of Space Mechanics & Electricity

Institute of Telecommunication and Navigation Satellites， China Academy of Space Technology

School of Informatics, Hunan University of Chinese Medicine

Key Laboratory of Medical Information Research （CSU）, College of Hunan Province

⁰