Multi-Core Reachability for Timed Automata

Andreas Dalsgaard, Alfons Laarman, K.G. Larsen, Mads Chr. Olesen, Jan Cornelis van de Pol

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    13 Citations (Scopus)
    68 Downloads (Pure)

    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.
    Original languageUndefined
    Title of host publication10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012
    EditorsM. Jurdzinski, D. Nickovic
    Place of PublicationLondon
    PublisherSpringer
    Pages91-106
    Number of pages16
    ISBN (Print)978-3-642-33365-1
    DOIs
    Publication statusPublished - 18 Sep 2012
    Event10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012 - Imperial College London, London, United Kingdom
    Duration: 18 Sep 201220 Sep 2012
    Conference number: 10
    http://www2.warwick.ac.uk/fac/cross_fac/dimap/events/formats2012/

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Volume7595
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012
    Abbreviated titleFORMATS
    CountryUnited Kingdom
    CityLondon
    Period18/09/1220/09/12
    Internet address

    Keywords

    • METIS-287893
    • Abstraction
    • IR-80819
    • Multi-Core
    • Model Checking
    • well-quasi-ordering
    • EWI-21972
    • lockless
    • lattice-based model checking
    • Timed Automata
    • Symbolic reachability
    • Parallel
    • FMT-MC: MODEL CHECKING
    • hash table

    Cite this

    Dalsgaard, A., Laarman, A., Larsen, K. G., Olesen, M. C., & van de Pol, J. C. (2012). Multi-Core Reachability for Timed Automata. In M. Jurdzinski, & D. Nickovic (Eds.), 10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012 (pp. 91-106). (Lecture Notes in Computer Science; Vol. 7595). London: Springer. https://doi.org/10.1007/978-3-642-33365-1_8