zbMATH — the first resource for mathematics

Multi-core reachability for timed automata. (English) Zbl 1374.68277
Jurdziński, Marcin (ed.) et al., Formal modeling and analysis of timed systems. 10th international conference, FORMATS 2012, London, UK, September 18-20, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-33364-4/pbk). Lecture Notes in Computer Science 7595, 91-106 (2012).
Summary: Model checking of timed automata is a widely used technique. But in order to take advantage of modern hardware, the algorithms need to be parallelized. We present a multi-core reachability algorithm 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 automaton 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 handle 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 current 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) parallel DFS search order are shown to reduce the state count, and improve speedups.
For the entire collection see [Zbl 1251.68022].
68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
Uppaal; opaal; LTSmin
Full Text: DOI