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

Clc Number:

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    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.

    Reference
    Related
    Cited by
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:February 23,2016
  • Revised:March 28,2016
  • Adopted:
  • Online: October 22,2016
  • Published:
Article QR Code
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-3
Address:4# South Fourth Street, Zhongguancun,Haidian, Beijing,Postal Code:100190
Phone:010-62661041 Fax: Email:csa (a) iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063