基于扩展RED图的概率时间自动机可达性分析

• 作者: 吴鹏 王凡 纪玮
• 来源期刊: 计算机系统应用
• 关键词: 概率时间自动机 可达性分析 RED图 扩展RED图
• 年，卷（期）: 2016,（10）
• 所属期刊栏目: 专论·综述
• 页码范围: 1-10
• 页数: 10页
• 字数: 7511字
• 语种: 中文
• DOI: 10.15888/j.cnki.csa.005414

摘要

RED图可以表示一个完整的时间自动机上的状态集,包括其连续时间部分和离散部分.在它基础上实现的模型检测工具RED,在时间自动机模型检测中表现出了优良的性能.另一方面,现有的概率时间自动机模型检测工具仍然使用不同的方法来分别表示概率时间自动机状态的连续时间和离散部分.我们在复用原始RED图的数据结构的基础上,对其做出了扩展,以令其支持概率状态的表达,同时保持其性能方面的优势.我们又为此实现了一个概率时间自动机可达性分析工具原型,并将其与两个概率模型检测工具(PRISM和Modest)就概率时间自动机可达性分析作实验对比,来评估该工具原型的性能.实验结果显示,我们的集成表示概率状态空间的方式,确实提高了概率时间自动机模型检测的时间效率和延展性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	吴鹏	中国科学院软件研究所计算机科学国家重点实验室	13	57	3.0	7.0
2	纪玮	中国科学院软件研究所计算机科学国家重点实验室	1	2	1.0	1.0