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

• 作者: 张君华 曹子宁 黄志球
• 来源期刊: 计算机研究与发展
• 学科: 工学
• 关键词: 模型检测 反例 基于概率时间自动机 符号状态交集 不确定性
• 年，卷（期）: 2008,（10）
• 所属期刊栏目: 可信计算
• 页码范围: 1638-1645
• 页数: 8页
• 分类号: TP311.5
• 字数: 7903字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	黄志球	南京航空航天大学计算机科学与技术系	183	1755	20.0	33.0
2	张君华	南京航空航天大学计算机科学与技术系	7	74	3.0	7.0
3	曹子宁	南京航空航天大学计算机科学与技术系	25	200	8.0	13.0