Multi-core reachability for timed automata

Abstract. Model checking of timed automata is a widely used tech-nique. But in order to take advantage of modern hardware, the algo-rithms need to be parallelized. We present a multi-core reachability al-gorithm for the more general class of well-structured transition systems, and an implementation for timed automata. Our implementation extends the opaal tool to generate a timed automa-ton successor generator in c++, that is efficient enough to compete with the uppaal model checker, and can be used by the discrete model checker LTSmin, whose parallel reachability algorithms are now extended to han-dle subsumption of semi-symbolic states. The reuse of efficient lockless data structures guarantees high scalability and efficient memory use. With experiments we show that opaal+LTSmin can outperform the cur-rent state-of-the-art, uppaal. The added parallelism is shown to reduce verification times from minutes to mere seconds with speedups of up to 40 on a 48-core machine. Finally, strict BFS and (surprisingly) paral-lel DFS search order are shown to reduce the state count, and improve speedups.