随机模型检测连续时间markov过程

功能正确和性能可满足是复杂系统可信要求非常重要的两个方面。从定性验证和定量分析相结合的角度，对复杂并发系统进行功能验证和性能分析，统一地评估系统是否可信。连续时间markov决策过程ctmdp(continuoustimemarkovdecisionprocess)能够统一刻画复杂系统的概率选择、随机时间及不确定性等重要特征。提出用ctmdp作为系统定性验证和定量分析模型，将复杂系统的功能验证和性能分析转化为ctmdp中的可达概率求解，并证明验证过程的正确性，最终借助模型检测器mrmc(markovrewardmodelchcckcr)实现模型检测。理论分析表明，提出的针对ci'mdp模型的验证需求是必要的，验证思路和方法具有可行性。