摘要
对系统模型进行验证是保证系统安全的一个关键.连续时间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.
出处
《广西科技大学学报》
CAS
2014年第3期59-62,86,共5页
Journal of Guangxi University of Science and Technology
基金
广西自然科学基金项目(2013GXNSFBA019280)
同济大学嵌入式与服务计算教育部重点实验室开放课题基金(2011-02)
广西高校科学技术研究项目(LX2014186)资助
关键词
马尔科夫决策过程
交互式马尔科夫链
时间有界可达概率
时间策略
Markov decision process
interactive Markov chains
time -bounded reachability probability
timedschedulers
