基于时间策略的连续时间Markov过程验证

Model checking Continuous time Markov Process based on timed Schedulers

对系统模型进行验证是保证系统安全的一个关键.连续时间Markov过程可以刻画复杂并发系统的随机、概率、不确定性特征.提出时间依赖策略下连续时间Markov过程验证方法,将连续时间Markov过程转换成为交互式马尔科夫链,给出模型的转换方法及不确定性选择策略的转换方法,最终通过求解交互式马尔科夫链的时间可达概率最值实现对连续时间Markov过程模型的验证.理论分析表明,提出的方法具有可行性.

System validation before implement is more important for safety critical systems. Continuous-time Markov decision process （CTMDP） is a model that contains some aspects such as probabilistic choice, stochastic timing and nondeterministic choice. In this paper, model checking continuous time Markov process based on timed schedulers is proposed. Firstly, the formal conversions of model and their nondeterministic choices schedulers from continuous time Markov decision process to interactive Markov chains are introduced. After then we reduce the problem of model checking for continuous time decision process to the problem of computing the maximum time- bounded teachability probabilities of interactive Markov chains. The theoretical analysis shows that the proposed approach is feasibility.