%0 Journal Article
%T 随机模型检测连续时间markov过程
%A 钮俊
%A 曾国荪
%A 吕新荣
%A 徐畅？
%J 计算机科学
%D 2011
%X 功能正确和性能可满足是复杂系统可信要求非常重要的两个方面。从定性验证和定量分析相结合的角度，对复杂并发系统进行功能验证和性能分析，统一地评估系统是否可信。连续时间markov决策过程ctmdp(continuoustimemarkovdecisionprocess)能够统一刻画复杂系统的概率选择、随机时间及不确定性等重要特征。提出用ctmdp作为系统定性验证和定量分析模型，将复杂系统的功能验证和性能分析转化为ctmdp中的可达概率求解，并证明验证过程的正确性，最终借助模型检测器mrmc(markovrewardmodelchcckcr)实现模型检测。理论分析表明，提出的针对ci'mdp模型的验证需求是必要的，验证思路和方法具有可行性。
%K 功能性能
%K 连续时间markov决策过程
%K 模型检测
%K 可信验证
%K 可达概率
%U http://www.jsjkx.com/jsjkx/ch/reader/view_abstract.aspx?file_no=110925&flag=1