Multi-Core Reachability for Timed Automata

Andreas Dalsgaard, Alfons Laarman, Kim G. Larsen, Mads Chr. Olesen, Jaco van de Pol

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

    13 Citations (Scopus)
    136 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 languageEnglish
    Title of host publicationFormal Modeling and Analysis of Timed Systems
    Subtitle of host publication10th International Conference, FORMATS 2012, London, UK, September 18-20, 2012, Proceedings
    EditorsMarcin Jurdziński, Dejan Ničković
    Place of PublicationBerlin, Heidelberg
    PublisherSpringer
    Pages91-106
    Number of pages16
    ISBN (Electronic)978-3-642-33365-1
    ISBN (Print)978-3-642-33365-1
    DOIs
    Publication statusPublished - 18 Sept 2012
    Event10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012 - Imperial College London, London, United Kingdom
    Duration: 18 Sept 201220 Sept 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
    Country/TerritoryUnited Kingdom
    CityLondon
    Period18/09/1220/09/12
    Internet address

    Keywords

    • Abstraction
    • Multi-Core
    • Model Checking
    • Well-quasi-ordering
    • Lockless
    • Lattice-based model checking
    • Timed automata
    • Symbolic reachability
    • Parallel
    • FMT-MC: MODEL CHECKING
    • Hash table

    Fingerprint

    Dive into the research topics of 'Multi-Core Reachability for Timed Automata'. Together they form a unique fingerprint.

    Cite this