首页|Model Checking Computation Tree Logic over Multi-Valued Decision Processes and Its Reduction Techniques
Model Checking Computation Tree Logic over Multi-Valued Decision Processes and Its Reduction Techniques
扫码查看
点击上方二维码区域,可以放大扫码查看
原文链接
万方数据
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 accur-ate 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 nondeter-minism 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 ex-pressed by using multi-valued computation tree logic based on schedulers.Our primary objective is to leverage fix-point 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 processesMulti-valued computation tree logicSchedulerReduction tech-niquesModel checking
Wuniu LIU、Junmei WANG、Qing HE、Yongming LI
展开 >
School of Mathematics and Statistics,Shaanxi Normal University,Xi'an 710119,China
School of Computer Science,Shaanxi Normal University,Xi'an 710119,China