TY - GEN
T1 - Deep random search for efficient model checking of timed automata
AU - Grosu, R.
AU - Huang, X.
AU - Smolka, S. A.
AU - Tan, W.
AU - Tripakis, S.
PY - 2007
Y1 - 2007
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/38549107869
M3 - Conference contribution
AN - SCOPUS:38549107869
SN - 3540774181
SN - 9783540774181
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 111
EP - 124
BT - Composition of Embedded Systems
T2 - 13th Monterey Workshop 2006 on Composition of Embedded Systems: Scientific and Industrial Issues
Y2 - 16 October 2006 through 18 October 2006
ER -