Model Checking Computation Tree Logic over Multi-Valued Decision Processes and Its Reduction Techniques  

作　　者：Wuniu LIU Junmei WANG Qing HE Yongming LI 

机构地区：[1]School of Mathematics and Statistics,Shaaxi Normal University,Xi'an 710119,China [2]School of Computer Science,Shaanxi Normal University,Xi'an 710119,China

出　　处：《Chinese Journal of Electronics》2024年第6期1399-1411,共13页电子学报（英文版）

基　　金：supported by the National Natural Science Foundation of China(Grant Nos.12071271 and 11671244);the Fundamental Research Funds for the C entral Universities(Grant No.2020CSLY016)。

摘　　要：Model checking computation tree logic based on multi-valued possibility measures has been studied by Li et al.on Information Sciences in 2019.However,the previous work did not consider the nondeterministic choices inherent in systems represented by multi-valued Kripke structures(MvKSs).This nondeterminism is crucial for accurate system modeling,decision making,and control capabilities.To address this limitation,we draw inspiration from the generalization of Markov chains to Markov decision processes in probabilistic systems.By integrating nondeterminism into MvKS,we introduce multi-valued decision processes(MvDPs)as a framework for modeling MvKSs with nondeterministic choices.We investigate the problems of model checking over MvDPs.Verifying properties are expressed by using multi-valued computation tree logic based on schedulers.Our primary objective is to leverage fixpoint techniques to determine the maximum and minimum possibilities of the system satisfying temporal properties.This allows us to identify the optimal or worst-case schedulers for decision making or control purposes.We aim to develop reduction techniques that enhance the efficiency of model checking,thereby reducing the associated time complexity.We mathematically demonstrate three reduction techniques that improve model checking performance in most scenarios.

关 键 词：Multi-valued decision processes Multi-valued computation tree logic SCHEDULER Reduction techniques Model checking 

分 类 号：O225[理学—运筹学与控制论]