Multi-core emptiness checking of timed Büchi automata using inclusion abstraction

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

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

    16 Citations (Scopus)
    14 Downloads (Pure)

    Abstract

    This paper contributes to the multi-core model checking of timed automata (TA) with respect to liveness properties, by investigating checking of TA Büchi emptiness under the very coarse inclusion abstraction or zone subsumption, an open problem in this field. We show that in general Büchi emptiness is not preserved under this abstraction. However, we prove that some other structural properties are preserved. Solving the problem partly, we propose a variation of the classic nested depth-first search (NDFS) algorithm that takes advantage of these properties thereby exploiting inclusion abstraction. In addition, we extend the multi-core CNDFS algorithm with subsumption, providing the first parallel LTL model checking algorithm for timed automata. We prove both algorithms correct and show that other, more aggressive variations are incorrect. The algorithms are implemented in LTSmin, and experimental evaluations show the effectiveness and scalability of both contributions: subsumption halves the number of states in the real-world FDDI and CSMA case studies, and the multi-core algorithm yields speedups of up to 40 on a 48 cores.
    Original languageEnglish
    Title of host publicationComputer Aided Verification
    Subtitle of host publication25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings
    EditorsNatasha Sharygina, Helmut Veith
    Place of PublicationLondon
    PublisherSpringer
    Pages968-983
    Number of pages18
    ISBN (Print)978-3-642-39798-1
    DOIs
    Publication statusPublished - 13 Jul 2013
    Event25th International Conference on Computer Aided Verification, CAV 2013 - Saint Petersburg, Russian Federation
    Duration: 13 Jul 201319 Jul 2013
    Conference number: 25

    Publication series

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

    Conference

    Conference25th International Conference on Computer Aided Verification, CAV 2013
    Abbreviated titleCAV
    CountryRussian Federation
    CitySaint Petersburg
    Period13/07/1319/07/13

    Fingerprint

    Model checking
    Carrier sense multiple access
    Scalability
    Structural properties

    Keywords

    • FMT-MC: MODEL CHECKING
    • METIS-296351
    • subsumption
    • inclusion abstraction
    • Timed Automata
    • UPPAAL
    • opaal
    • Parallel
    • LTL
    • LTSMIN
    • LU abstraction
    • liveness
    • Model Checking
    • Multi-Core
    • NDFS
    • Büchi emptiness
    • IR-84627
    • CNDFS
    • EWI-23158

    Cite this

    Laarman, A., Olesen, M. C., Dalsgaard, A., Larsen, K. G., & van de Pol, J. (2013). Multi-core emptiness checking of timed Büchi automata using inclusion abstraction. In N. Sharygina, & H. Veith (Eds.), Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings (pp. 968-983). (Lecture Notes in Computer Science; Vol. 8044). London: Springer. https://doi.org/10.1007/978-3-642-39799-8_69
    Laarman, Alfons ; Olesen, Mads Chr. ; Dalsgaard, Andreas ; Larsen, Kim G. ; van de Pol, Jaco . / Multi-core emptiness checking of timed Büchi automata using inclusion abstraction. Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. editor / Natasha Sharygina ; Helmut Veith. London : Springer, 2013. pp. 968-983 (Lecture Notes in Computer Science).
    @inproceedings{4ec02d4bc50041349c7f36c9407c8de0,
    title = "Multi-core emptiness checking of timed B{\"u}chi automata using inclusion abstraction",
    abstract = "This paper contributes to the multi-core model checking of timed automata (TA) with respect to liveness properties, by investigating checking of TA B{\"u}chi emptiness under the very coarse inclusion abstraction or zone subsumption, an open problem in this field. We show that in general B{\"u}chi emptiness is not preserved under this abstraction. However, we prove that some other structural properties are preserved. Solving the problem partly, we propose a variation of the classic nested depth-first search (NDFS) algorithm that takes advantage of these properties thereby exploiting inclusion abstraction. In addition, we extend the multi-core CNDFS algorithm with subsumption, providing the first parallel LTL model checking algorithm for timed automata. We prove both algorithms correct and show that other, more aggressive variations are incorrect. The algorithms are implemented in LTSmin, and experimental evaluations show the effectiveness and scalability of both contributions: subsumption halves the number of states in the real-world FDDI and CSMA case studies, and the multi-core algorithm yields speedups of up to 40 on a 48 cores.",
    keywords = "FMT-MC: MODEL CHECKING, METIS-296351, subsumption, inclusion abstraction, Timed Automata, UPPAAL, opaal, Parallel, LTL, LTSMIN, LU abstraction, liveness, Model Checking, Multi-Core, NDFS, B{\"u}chi emptiness, IR-84627, CNDFS, EWI-23158",
    author = "Alfons Laarman and Olesen, {Mads Chr.} and Andreas Dalsgaard and Larsen, {Kim G.} and {van de Pol}, Jaco",
    year = "2013",
    month = "7",
    day = "13",
    doi = "10.1007/978-3-642-39799-8_69",
    language = "English",
    isbn = "978-3-642-39798-1",
    series = "Lecture Notes in Computer Science",
    publisher = "Springer",
    pages = "968--983",
    editor = "Natasha Sharygina and Helmut Veith",
    booktitle = "Computer Aided Verification",

    }

    Laarman, A, Olesen, MC, Dalsgaard, A, Larsen, KG & van de Pol, J 2013, Multi-core emptiness checking of timed Büchi automata using inclusion abstraction. in N Sharygina & H Veith (eds), Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. Lecture Notes in Computer Science, vol. 8044, Springer, London, pp. 968-983, 25th International Conference on Computer Aided Verification, CAV 2013, Saint Petersburg, Russian Federation, 13/07/13. https://doi.org/10.1007/978-3-642-39799-8_69

    Multi-core emptiness checking of timed Büchi automata using inclusion abstraction. / Laarman, Alfons; Olesen, Mads Chr.; Dalsgaard, Andreas; Larsen, Kim G.; van de Pol, Jaco .

    Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. ed. / Natasha Sharygina; Helmut Veith. London : Springer, 2013. p. 968-983 (Lecture Notes in Computer Science; Vol. 8044).

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

    TY - GEN

    T1 - Multi-core emptiness checking of timed Büchi automata using inclusion abstraction

    AU - Laarman, Alfons

    AU - Olesen, Mads Chr.

    AU - Dalsgaard, Andreas

    AU - Larsen, Kim G.

    AU - van de Pol, Jaco

    PY - 2013/7/13

    Y1 - 2013/7/13

    N2 - This paper contributes to the multi-core model checking of timed automata (TA) with respect to liveness properties, by investigating checking of TA Büchi emptiness under the very coarse inclusion abstraction or zone subsumption, an open problem in this field. We show that in general Büchi emptiness is not preserved under this abstraction. However, we prove that some other structural properties are preserved. Solving the problem partly, we propose a variation of the classic nested depth-first search (NDFS) algorithm that takes advantage of these properties thereby exploiting inclusion abstraction. In addition, we extend the multi-core CNDFS algorithm with subsumption, providing the first parallel LTL model checking algorithm for timed automata. We prove both algorithms correct and show that other, more aggressive variations are incorrect. The algorithms are implemented in LTSmin, and experimental evaluations show the effectiveness and scalability of both contributions: subsumption halves the number of states in the real-world FDDI and CSMA case studies, and the multi-core algorithm yields speedups of up to 40 on a 48 cores.

    AB - This paper contributes to the multi-core model checking of timed automata (TA) with respect to liveness properties, by investigating checking of TA Büchi emptiness under the very coarse inclusion abstraction or zone subsumption, an open problem in this field. We show that in general Büchi emptiness is not preserved under this abstraction. However, we prove that some other structural properties are preserved. Solving the problem partly, we propose a variation of the classic nested depth-first search (NDFS) algorithm that takes advantage of these properties thereby exploiting inclusion abstraction. In addition, we extend the multi-core CNDFS algorithm with subsumption, providing the first parallel LTL model checking algorithm for timed automata. We prove both algorithms correct and show that other, more aggressive variations are incorrect. The algorithms are implemented in LTSmin, and experimental evaluations show the effectiveness and scalability of both contributions: subsumption halves the number of states in the real-world FDDI and CSMA case studies, and the multi-core algorithm yields speedups of up to 40 on a 48 cores.

    KW - FMT-MC: MODEL CHECKING

    KW - METIS-296351

    KW - subsumption

    KW - inclusion abstraction

    KW - Timed Automata

    KW - UPPAAL

    KW - opaal

    KW - Parallel

    KW - LTL

    KW - LTSMIN

    KW - LU abstraction

    KW - liveness

    KW - Model Checking

    KW - Multi-Core

    KW - NDFS

    KW - Büchi emptiness

    KW - IR-84627

    KW - CNDFS

    KW - EWI-23158

    U2 - 10.1007/978-3-642-39799-8_69

    DO - 10.1007/978-3-642-39799-8_69

    M3 - Conference contribution

    SN - 978-3-642-39798-1

    T3 - Lecture Notes in Computer Science

    SP - 968

    EP - 983

    BT - Computer Aided Verification

    A2 - Sharygina, Natasha

    A2 - Veith, Helmut

    PB - Springer

    CY - London

    ER -

    Laarman A, Olesen MC, Dalsgaard A, Larsen KG, van de Pol J. Multi-core emptiness checking of timed Büchi automata using inclusion abstraction. In Sharygina N, Veith H, editors, Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. London: Springer. 2013. p. 968-983. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-39799-8_69