概率时段演算的模型检验概述

摘要：

在实际工程应用中，越来越多的系统表现出具有概率性等特征。作为对于此类实时系统的建模，概率时间自动机因为其能同时表示概率性、随机性和不确定性而被广泛采用。在对此类带概率性质的实时系统进行描述时，作为时段演算的一种扩展，概率时段演算被用来计算此类系统满足需求的概率。该文主要概述基于概率时间自动机的概率时段演算的模型检验主要步骤及其核心算法，其中模型检验的核心算法通过分别将前两者转换为区域图和概率分支时间逻辑来达成。

关键词：实时系统、模型检验、概率时间自动机、概率时段演算

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

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

页数：共3页

页码：8171-8173