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

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

Markov决策过程不确定策略特征模式

马尔科夫决策过程可以建模具有不确定性特征的复杂系统,而在进行模型分析时需要采用策略对不确定性进行处理。首先,研究不同策略下时空有界可达概率问题,给出不确定性解决策略的定义及分类方法。其次,在时间无关策略下,证明基于确定性选取动作和随机选取动作的时空有界可达概率的一致性,并且论证了时间依赖策略相对于时间无关策略具有更好的时空有界可达概率。最后结合实例简要阐述了结论的正确性。

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

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

代价和概率时间自动机上概率有界的成本优化可达性

着重解决代价和概率时间自动机模型的可达性问题,即满足一定概率要求的最小代价问题。在该模型中搜索满足概率要求的路径,据此路径构造相应的代价时间自动机,求解此路径的最小代价,从而求得满足概率要求的总的最小代价。另外,通过扩展代价和概率时间自动机模型,得到多代价和概率时间自动机。相应的可达性问题,即满足一定概率要求的符合辅助成本约束的主成本最小代价问题,也可类似地得到解决。

带动作回报的连续时间Markov回报过程验证

为了能够更准确的表达不确定性复杂系统的时空验证,针对当前连续时间Markov回报过程(continue time markov reward decision process,CMRDP)验证中只考虑状态回报的问题,提出带动作回报的验证方法。考虑添加了动作回报的空间性能约束,扩展现有的基于状态回报的连续时间Markov回报过程,用正则表达式表示验证属性的路径规范,扩展已有路径算子的表达能力。给出带动作回报CMRDP和路径规范的积模型,求解积模型在确定性策略下的诱导Markov回报模型(markov reward model,MRM),将CMRDP上的时空性能验证转换为MRM模型上的时空可达概率分析,并提出MRM中求解可达概率的算法。实例分析表明,提出的验证思路和验证算法是可行的。