摘要： 根据带有随机特征的复杂信息系统性质验证的需求，针对离散概率回报模型的分层直到公式，提出一种性质验证分析方法。在综合各种离散随机逻辑的基础上，使用一种同时具有迁移回报及迁移步区间表达能力的概率计算树逻辑表示系统模型的分层直到路径公式性质，使用自动机技术建模路径公式，通过构造积模型完成模型与自动机的同步演化，基于积模型给出相应的状态概率满足算法。实例结果验证了该方法的可行性和有效性。

关键词: 模型检测, 分层直到公式, 概率计算树逻辑, 马尔可夫链, 自动机, 积模型

Abstract: According to the demand of property verification for complex information system with random nature, this paper presents a kind of stratified until formula properties verification and analysis method acting on discrete probability rewards model. A new more expressive probabilistic computation tree logic both with transition reward interval and transition step interval expression ability is used to describe stratified until formula properties of system model on the basis of all kinds of discrete stochastic logic variants. By using automaton to express logic path formula, the corresponding state probability satisfaction algorithm is described based on product model which realizes the simultaneous evolution of the model and the automaton. The example result verifies the feasibility and validity of the method.

Key words: model check, stratified until formula, probabilistic computation tree logic, Markov chain, automaton, product model

中图分类号: 

• TP311