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.
Revised Selected Papers of MW'06, the 7th Monterey Workshop on Composition of Embedded Systems, October, 2006, Paris, France, Springer LNCS 4888, pp. 111-1124, 2007.
*This work was partially supported by the NSF Faculty Early Career
Development Award CCR01-33583 and the NSF CSR-AES05-09230 Award.