Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking

J. Barnat, L. Brim, P. Šimeček, M. Weber

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

    20 Citations (Scopus)

    Abstract

    Revisiting resistant graph algorithms are those that can tolerate re-exploration of edges without yielding incorrect results. Revisiting resistant I/O efficient graph algorithms exhibit considerable speed-up in practice in comparison to non-revisiting resistant algorithms. In the paper we present a new revisiting resistant I/O efficient LTL model checking algorithm. We analyze its theoretical I/O complexity and we experimentally compare its performance to already existing I/O efficient LTL model checking algorithms.
    Original languageUndefined
    Title of host publication14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008
    EditorsC.R. Ramakrishnan, J Rehof
    Place of PublicationLondon
    PublisherSpringer
    Pages48-62
    Number of pages14
    ISBN (Print)978-3-540-78799-0
    DOIs
    Publication statusPublished - Mar 2008

    Publication series

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

    Keywords

    • EWI-12954
    • METIS-251039
    • IR-62369

    Cite this

    Barnat, J., Brim, L., Šimeček, P., & Weber, M. (2008). Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking. In C. R. Ramakrishnan, & J. Rehof (Eds.), 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008 (pp. 48-62). [10.1007/978-3-540-78800-3_5] (Lecture Notes in Computer Science; Vol. 4963, No. 302). London: Springer. https://doi.org/10.1007/978-3-540-78800-3_5
    Barnat, J. ; Brim, L. ; Šimeček, P. ; Weber, M. / Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking. 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008. editor / C.R. Ramakrishnan ; J Rehof. London : Springer, 2008. pp. 48-62 (Lecture Notes in Computer Science; 302).
    @inproceedings{6c4a2ad547fc454aaa413b3a41ca9434,
    title = "Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking",
    abstract = "Revisiting resistant graph algorithms are those that can tolerate re-exploration of edges without yielding incorrect results. Revisiting resistant I/O efficient graph algorithms exhibit considerable speed-up in practice in comparison to non-revisiting resistant algorithms. In the paper we present a new revisiting resistant I/O efficient LTL model checking algorithm. We analyze its theoretical I/O complexity and we experimentally compare its performance to already existing I/O efficient LTL model checking algorithms.",
    keywords = "EWI-12954, METIS-251039, IR-62369",
    author = "J. Barnat and L. Brim and P. Šimeček and M. Weber",
    note = "10.1007/978-3-540-78800-3_5",
    year = "2008",
    month = "3",
    doi = "10.1007/978-3-540-78800-3_5",
    language = "Undefined",
    isbn = "978-3-540-78799-0",
    series = "Lecture Notes in Computer Science",
    publisher = "Springer",
    number = "302",
    pages = "48--62",
    editor = "C.R. Ramakrishnan and J Rehof",
    booktitle = "14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008",

    }

    Barnat, J, Brim, L, Šimeček, P & Weber, M 2008, Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking. in CR Ramakrishnan & J Rehof (eds), 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008., 10.1007/978-3-540-78800-3_5, Lecture Notes in Computer Science, no. 302, vol. 4963, Springer, London, pp. 48-62. https://doi.org/10.1007/978-3-540-78800-3_5

    Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking. / Barnat, J.; Brim, L.; Šimeček, P.; Weber, M.

    14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008. ed. / C.R. Ramakrishnan; J Rehof. London : Springer, 2008. p. 48-62 10.1007/978-3-540-78800-3_5 (Lecture Notes in Computer Science; Vol. 4963, No. 302).

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

    TY - GEN

    T1 - Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking

    AU - Barnat, J.

    AU - Brim, L.

    AU - Šimeček, P.

    AU - Weber, M.

    N1 - 10.1007/978-3-540-78800-3_5

    PY - 2008/3

    Y1 - 2008/3

    N2 - Revisiting resistant graph algorithms are those that can tolerate re-exploration of edges without yielding incorrect results. Revisiting resistant I/O efficient graph algorithms exhibit considerable speed-up in practice in comparison to non-revisiting resistant algorithms. In the paper we present a new revisiting resistant I/O efficient LTL model checking algorithm. We analyze its theoretical I/O complexity and we experimentally compare its performance to already existing I/O efficient LTL model checking algorithms.

    AB - Revisiting resistant graph algorithms are those that can tolerate re-exploration of edges without yielding incorrect results. Revisiting resistant I/O efficient graph algorithms exhibit considerable speed-up in practice in comparison to non-revisiting resistant algorithms. In the paper we present a new revisiting resistant I/O efficient LTL model checking algorithm. We analyze its theoretical I/O complexity and we experimentally compare its performance to already existing I/O efficient LTL model checking algorithms.

    KW - EWI-12954

    KW - METIS-251039

    KW - IR-62369

    U2 - 10.1007/978-3-540-78800-3_5

    DO - 10.1007/978-3-540-78800-3_5

    M3 - Conference contribution

    SN - 978-3-540-78799-0

    T3 - Lecture Notes in Computer Science

    SP - 48

    EP - 62

    BT - 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008

    A2 - Ramakrishnan, C.R.

    A2 - Rehof, J

    PB - Springer

    CY - London

    ER -

    Barnat J, Brim L, Šimeček P, Weber M. Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking. In Ramakrishnan CR, Rehof J, editors, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008. London: Springer. 2008. p. 48-62. 10.1007/978-3-540-78800-3_5. (Lecture Notes in Computer Science; 302). https://doi.org/10.1007/978-3-540-78800-3_5