综合特征Markov模型稳态性质验证方法

Steady-state property verification method of Markov model with integrated characteristics

针对带有复杂参数特征的信息系统性质验证需求,提出一种作用于连续概率奖励模型的稳态公式性质验证分析方法。使用具有综合特征表示能力的连续时间马尔可夫决策过程作为系统定量分析模型,采用连续随机奖励逻辑描述系统的性质,通过不确定性消解、离散化处理、状态消去等方法,实现了原模型中稳态概率的近似求解。理论分析及实例结果表明了该方法的可行性和有效性。

To meet the demand of property verification for information system with complex parametric nature, a kind of steadystate formula properties verification and analysis method acting on continuous probability rewards model is proposed. The continuous time Markov decision process with comprehensive feature is used as the system model of quantitative analysis and the continuous stochastic reward logic is used to describe the nature of the system, through the specific methods, such as uncertainty digestion, discretization treatment and state elimination, finally the approximate solution of steady-state probability is achieved. The theoretical analysis and example result shows the feasibility and validity of verification method.