https://scholars.lib.ntu.edu.tw/handle/123456789/497154
標題: | An Experiment on Decision Diagrams for Model Checking Probabilistic Timed Automata | 作者: | Ji, W. Wu, P. Lv, Y. FARN WANG |
關鍵字: | Probabilistic Model Checking; Probabilistic Timed Automata; Real-Time Systems; RED Diagrams; Symbolic Model Checking | 公開日期: | 2017 | 起(迄)頁: | 111-121 | 來源出版物: | Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS | 摘要: | The state-of-the-art model-checkers for probabilistic timed automata (PTAs) use separate representations for the dense-time and discrete parts of PTA states. In the literature, integrated state-space representations based on decision diagrams, e.g., RED diagrams (the underlying symbolic representation in the model checker RED), have shown considerable performance enhancement in model-checking timed automata (TAs) and linear hybrid automata (LHAs). A RED diagram for a TA can represent the dense-time and discrete parts of TA states in a single and integrated decision diagram. In this work, we experiment to investigate whether such performance enhancement can be duplicated with PTA model-checking. Specifically, we propose a lightweight extension to RED diagrams to represent quantitative states of PTAs in an integrated manner, yet preserving the structure-sharing capacity of RED diagrams. We then develop and implement a symbolic reachability analysis algorithm for PTAs based on the extended RED diagrams. We further carry out experiments with the PTA benchmarks from a popular probabilistic model checker PRISM to evaluate the performance of such integrated decision diagrams and the reachability analysis algorithm. Experimental results show that our approach can indeed help to improve the time-efficiency and scalability of PTA model-checking. © 2016 IEEE. |
URI: | https://www.scopus.com/inward/record.uri?eid=2-s2.0-85012066485&doi=10.1109%2fICECCS.2016.022&partnerID=40&md5=3adc2a4aecac523a9e6d5a6ac5182b5a | DOI: | 10.1109/ICECCS.2016.022 | SDG/關鍵字: | Automata theory; Benchmarking; Decision theory; Graphic methods; Interactive computer systems; Real time systems; State space methods; Performance enhancements; Probabilistic model checking; Probabilistic timed automata; RED Diagrams; State space representation; Symbolic model checking; Symbolic reachability analysis; Symbolic representation; Model checking |
顯示於: | 電機工程學系 |
在 IR 系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。