Multi-Core Reachability for Timed Automata


Dalsgaard, Andreas and Laarman, Alfons and Larsen, Kim G. and Olesen, Mads Chr. and Pol, Jaco van de (2012) Multi-Core Reachability for Timed Automata. In: 10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012, 18-20 September 2012, London, UK (pp. pp. 91-106).

[img] PDF
Restricted to UT campus only
: Request a copy
Abstract: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.
Item Type:Conference or Workshop Item
Copyright:© 2012 Springer
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:
Official URL:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 287893