Computation Tree Logic Model Checking over Possibilistic Decision Processes Under Finite-Memory Scheduler

Possibilistic model checking has been studied extensively, but the nondeterministic actions contained in the system are absent in previous possibilistic model checking. In order to add this nondeterminism to the model, we introduce the notion of generalized possibilistic decision processes (GPDP, in short) in this paper. We propose the scheduler to solve the nondeterminism of actions. We study the model checking under finite-memory scheduler, i.e., giving a GPDP, a finite-memory scheduler and a generalized possibilistic computation tree logic (GPoCTL) formula, compute its possibility under this scheduler. What's more, a method based on Entropy-weight TOPSIS is given to select the optimal schedulers from all given schedulers over possibility and necessity measures.