Abstract: Aiming at the model checking problem of uncertain fuzzy systems generated by data representation, a model checking algorithm of fuzzy computational tree logic is given.First of all, the fuzzy decision-making process is introduced as the model of this type of system. Its biggest feature is the uncertain choice of actions and the ambiguity of state expression during the migration process. Then, based on the fuzzy decision-making process, the grammar and semantics of fuzzy computation tree logic are given. Finally, a model detection algorithm of fuzzy computational tree logic is given. The algorithm is a synthetic operation that converts the model detection problem of fuzzy computational tree logic into a fuzzy matrix. Its advantages are low time complexity and a relatively simple calculation process.  

Key words: model checking, nondeterministic system, fuzzy decision process, fuzzy computation tree logic, fuzzy matrix