基于扩展RED图的概率时间自动机可达性分析
CSTR:
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

国家高技术研究发展计划(863)(2012AA010905);国家自然科学基金(61370081)


Reachability Analysis of Probabilistic Timed Automata Based on Extended RED Diagrams
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    Abstract:

    RED diagrams represent states of a timed automata in a single and integrated diagram for both the dense-time and the discrete parts of the states. This integration contributes greatly to the considerable efficiency of the model checker RED in verification of timed automata. On the other hand, the state-of-the-art model checkers for probabilistic timed automata (PTAs) still use different representations for the dense-time and the discrete parts of probabilistic states. This paper proposes an elegant way to extend RED diagrams to represent probabilistic states, yet reuses the structures of original RED diagrams and hence preserves their efficiency. It also implements a prototype tool for reachability analysis of PTAs based on the extended RED diagrams, while the PTA benchmarks distributed within the probabilistic model checkers PRISM and Modest are used to evaluate its performance. Experimental results show that our integrated representation of probabilistic state space can indeed help improve the time efficiency and scalability for PTA reachability analysis.

    参考文献
    相似文献
    引证文献
引用本文

纪玮,王凡,吴鹏.基于扩展RED图的概率时间自动机可达性分析.计算机系统应用,2016,25(10):1-10

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2016-02-23
  • 最后修改日期:2016-03-28
  • 录用日期:
  • 在线发布日期: 2016-10-22
  • 出版日期:
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京海淀区中关村南四街4号 中科院软件园区 7号楼305房间,邮政编码:100190
电话:010-62661041 传真: Email:csa (a) iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号