In order to solve the problems in fuzzy computation tree logic model checking with cost operator, we propose a fuzzy decision process computation tree logic model checking method with cost. Firstly, we introduce a fuzzy decision process model with cost, which can not only describe the uncertain choice and transition possibility of systems, but also quantitatively describe the cost of the systems. Secondly, under the model of the fuzzy decision process with cost, we give the syntax and semantics of the fuzzy computation tree logic with cost operators. Thirdly, we study the problem of computation tree logic model checking for fuzzy decision process with cost, and give its matrix calculation method and algorithm. We use the example of medical expert systems to illustrate the method and model checking algorithm.

In this paper, we focus on the symmetrical relationship between multi-properties objective reachability problems and multi-objective sets reachability problems over FKS based on Zadeh logic. First, we give the formal definitions of those two problems. Then, we study their relationships and find that a multi-properties objective reachability problem and a special case of multi-objective sets reachability problems have symmetry. Finally, we give a polynomial time algorithm based on this symmetry to convert a multi-properties objective reachability problem to a multi-objective sets reachability problem. In addition, an illustrative example is listed to express some possible application methods based on our work.