基于自动机的概率计算树逻辑验证方法

摘要：

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

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

分类号：TP311(计算技术、计算机技术)

资助基金：中央高校基本科研业务费专项基金资助项目DL11BB08；国家自然科学基金资助项目71001023

在线出版日期：2013-12-30（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：285-289