We present DRS (Deep Random Search), a new Las Vegas algorithm for model checking safety properties of timed automata. DRS explores the state space of the simulation graph of a timed automaton by performing random walks up to a prescribed depth. Nodes along these walks are then used to construct a random fringe, which is the starting point of additional deep random walks. The DRS algorithm is complete, and optimal to within a specified depth increment. Experimental results show that it is able to find extremely deep counter-examples for a number of benchmarks, outperforming Open-Kronos and UPPAAL in the process. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Grosu, R., Huang, X., Smolka, S. A., Tan, W., & Tripakis, S. (2007). Deep random search for efficient model checking of timed automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4888 LNCS, pp. 111–124). https://doi.org/10.1007/978-3-540-77419-8_7
Mendeley helps you to discover research relevant for your work.