Efficient simulation-based verification of probabilistic timed automata

TitleEfficient simulation-based verification of probabilistic timed automata
Publication TypeBook Chapter
Year of Publication2017
AuthorsHartmanns, A, Sedwards, S, D'Argenio, PR
Book Title2017 Winter Simulation Conference, {WSC} 2017, Las Vegas, NV, USA, December 3-6, 2017
Pagination1419–1430
Publisher{IEEE}
ISBN Number978-1-5386-3428-8
AbstractProbabilistic timed automata are a formal model for real-time systems with discrete probabilistic and nondeterministic choices. To overcome the state space explosion problem of exhaustive verification, a symbolic simulation-based approach that soundly treats nondeterminism to approximate maximum and minimum reachability probabilities has recently become available. Its use of difference-bound matrices to handle continuous real time however leads to poor performance: most operations are cubic or even exponential in the number of clock variables. In this paper, we propose a novel region-based approach and data structure that reduce the complexity of all operations to being linear. It relies on a particular mapping between symbolic regions and concrete representative valuations. Using an implementation within the MODEST TOOLSET, we show that the new approach is not only easier to implement, but indeed significantly outperforms all current alternatives on standard benchmark models.
URLhttps://doi.org/10.1109/WSC.2017.8247885
DOI10.1109/WSC.2017.8247885
PDF (Full text):