Based on the generalized possibilistic Kripke structure, possibilistic fuzzy linear temporal logic, GPoCTL* and generalized possibility measure, this article studies the model-checking problems of generalized possibilistic fuzzy CTL* (GPoFCTL*). GPoFCTL* includes fuzzy temporal logic operators such as “soon”, “presently”, “gradually”, “last”, “within”,“finally”, “nearly always”, “almost always”, “in the distant future”, “in the middle”, “almost until”, “nearly until”. This paper studies the syntax of GPoFCTL* and its semantics based on generalized possibility measures. In addition, we present an model checking algorithm for GPoFCTL* using fuzzy matrix operations. Finally, we present an example to illustrate the computational process of the model checking algorithm.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Generalized Possibilistic CTL* Model Checking with Fuzzy Temporal Logic Operators

  • Chuanjiang Mu,
  • Wuniu Liu,
  • Yongming Li

摘要

Based on the generalized possibilistic Kripke structure, possibilistic fuzzy linear temporal logic, GPoCTL* and generalized possibility measure, this article studies the model-checking problems of generalized possibilistic fuzzy CTL* (GPoFCTL*). GPoFCTL* includes fuzzy temporal logic operators such as “soon”, “presently”, “gradually”, “last”, “within”,“finally”, “nearly always”, “almost always”, “in the distant future”, “in the middle”, “almost until”, “nearly until”. This paper studies the syntax of GPoFCTL* and its semantics based on generalized possibility measures. In addition, we present an model checking algorithm for GPoFCTL* using fuzzy matrix operations. Finally, we present an example to illustrate the computational process of the model checking algorithm.