An Experiment on Decision Diagrams for Model Checking Probabilistic Timed Automata
Journal
Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS
Pages
111-121
Date Issued
2017
Author(s)
Abstract
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.
Subjects
Probabilistic Model Checking; Probabilistic Timed Automata; Real-Time Systems; RED Diagrams; Symbolic Model Checking
SDGs
Other Subjects
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
Type
conference paper