首页|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

2024

电子学报(英文)

电子学报(英文)

CSTPCDEI
ISSN:1022-4653
年,卷(期):2024.33(6)