模型检测基于概率时间自动机的反例产生研究

被引：6

作者：

张君华

黄志球

曹子宁

机构：

[1] 南京航空航天大学计算机科学与技术系

来源：

计算机研究与发展 | 2008年 / 10期

关键词：

模型检测; 反例; 基于概率时间自动机; 符号状态交集; 不确定性;

D O I：

暂无

中图分类号：

TP311.52 [];

学科分类号：

081202 ; 0835 ;

摘要：

模型检测基于概率系统的反例产生问题,在最近引起人们的关注.已有的工作主要围绕模型检测Markov链的反例产生而开展.基于概率时间自动机(PTA)是Markov链的不确定性和系统时钟的扩展.关注的是模型检测PTA的反例产生问题.首先通过在PTA上寻找概率之和恰好大于λ的k条最大概率的路径,并根据这些路径和原PTA构造原PTA的一个子图,从而快速找到违背性质的具有较少证据的反例.然后精化此结果——通过逐条加入上述各条最大概率的路径来精确地计算已加入路径所构成的PTA子图的最大概率.由于考虑到符号状态交集对概率系统的影响,可以得到证据更少的反例.

引用

页码：1638 / 1645

页数：8

共 3 条

[1] 基于Horn逻辑扩展模型的安全协议反例的自动构造 [J].

周倜 ;

李梦君 ;

李舟军 ;

陈火旺 .

计算机研究与发展, 2007, (09) :1518-1531

[2] Fate and free will in error traces [J].

Jin H. ;

Ravi K. ;

Somenzi F. .

International Journal on Software Tools for Technology Transfer, 2004, 6 (2) :102-116

[3]

Probabilistic Model Checking of Deadline Properties in the IEEE 1394 FireWire Root Contention Protocol[J] . Marta Kwiatkowska,Gethin Norman,Jeremy Sproston.Formal Aspects of Computing . 2003 (3)

← 1 →