Generalized Possibilistic CTL* Model Checking with Fuzzy Temporal Logic Operators
摘要
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.