Speedup of OWCTY model checking algorithm using strongly connected components

Toshiki Kawabata, Fumiyoshi Kobayashi, Kazunori Ueda

    Research output: Contribution to journalArticle

    Abstract

    Model checking is an exhaustive search method of verification. Automata-based LTL model checking is one of the methods to solve accepting cycle search problems. Model checking is prone to state-space explosion, and we may expect that parallel processing would be a promising approach. However, the optimal sequential algorithm is based on post-order depth-first seach and is difficult to parallelize. Alternative parallel algorithms have been proposed, and OWCTY_reversed is one of them. OWCTY_reversed is known to be a stable and fast algorithmfor models that accept some words, but it does not use the characteristics of the automata used in LTL model checking. We propose a new algorithm named SCC-OWCTY that exploits the SCCs (strongly connected components) of property automata. The algorithmremoves states that are judged not to form accepting cycles faster than OWCTY_reversed. We experimented and compared the two algorithms using DiVinE, and confirmed improvements both in performance and scalability.

    Original languageEnglish
    Pages (from-to)341-346
    Number of pages6
    JournalTransactions of the Japanese Society for Artificial Intelligence
    Volume26
    Issue number2
    DOIs
    Publication statusPublished - 2011

    Fingerprint

    Model checking
    Parallel algorithms
    Explosions
    Scalability
    Processing

    Keywords

    • Accepting cycle search
    • Model checking
    • Parallelization
    • Strongly connected components

    ASJC Scopus subject areas

    • Artificial Intelligence
    • Software

    Cite this

    Speedup of OWCTY model checking algorithm using strongly connected components. / Kawabata, Toshiki; Kobayashi, Fumiyoshi; Ueda, Kazunori.

    In: Transactions of the Japanese Society for Artificial Intelligence, Vol. 26, No. 2, 2011, p. 341-346.

    Research output: Contribution to journalArticle

    @article{6a4f995b8a164eff977916f8b54663c9,
    title = "Speedup of OWCTY model checking algorithm using strongly connected components",
    abstract = "Model checking is an exhaustive search method of verification. Automata-based LTL model checking is one of the methods to solve accepting cycle search problems. Model checking is prone to state-space explosion, and we may expect that parallel processing would be a promising approach. However, the optimal sequential algorithm is based on post-order depth-first seach and is difficult to parallelize. Alternative parallel algorithms have been proposed, and OWCTY_reversed is one of them. OWCTY_reversed is known to be a stable and fast algorithmfor models that accept some words, but it does not use the characteristics of the automata used in LTL model checking. We propose a new algorithm named SCC-OWCTY that exploits the SCCs (strongly connected components) of property automata. The algorithmremoves states that are judged not to form accepting cycles faster than OWCTY_reversed. We experimented and compared the two algorithms using DiVinE, and confirmed improvements both in performance and scalability.",
    keywords = "Accepting cycle search, Model checking, Parallelization, Strongly connected components",
    author = "Toshiki Kawabata and Fumiyoshi Kobayashi and Kazunori Ueda",
    year = "2011",
    doi = "10.1527/tjsai.26.341",
    language = "English",
    volume = "26",
    pages = "341--346",
    journal = "Transactions of the Japanese Society for Artificial Intelligence",
    issn = "1346-0714",
    publisher = "Japanese Society for Artificial Intelligence",
    number = "2",

    }

    TY - JOUR

    T1 - Speedup of OWCTY model checking algorithm using strongly connected components

    AU - Kawabata, Toshiki

    AU - Kobayashi, Fumiyoshi

    AU - Ueda, Kazunori

    PY - 2011

    Y1 - 2011

    N2 - Model checking is an exhaustive search method of verification. Automata-based LTL model checking is one of the methods to solve accepting cycle search problems. Model checking is prone to state-space explosion, and we may expect that parallel processing would be a promising approach. However, the optimal sequential algorithm is based on post-order depth-first seach and is difficult to parallelize. Alternative parallel algorithms have been proposed, and OWCTY_reversed is one of them. OWCTY_reversed is known to be a stable and fast algorithmfor models that accept some words, but it does not use the characteristics of the automata used in LTL model checking. We propose a new algorithm named SCC-OWCTY that exploits the SCCs (strongly connected components) of property automata. The algorithmremoves states that are judged not to form accepting cycles faster than OWCTY_reversed. We experimented and compared the two algorithms using DiVinE, and confirmed improvements both in performance and scalability.

    AB - Model checking is an exhaustive search method of verification. Automata-based LTL model checking is one of the methods to solve accepting cycle search problems. Model checking is prone to state-space explosion, and we may expect that parallel processing would be a promising approach. However, the optimal sequential algorithm is based on post-order depth-first seach and is difficult to parallelize. Alternative parallel algorithms have been proposed, and OWCTY_reversed is one of them. OWCTY_reversed is known to be a stable and fast algorithmfor models that accept some words, but it does not use the characteristics of the automata used in LTL model checking. We propose a new algorithm named SCC-OWCTY that exploits the SCCs (strongly connected components) of property automata. The algorithmremoves states that are judged not to form accepting cycles faster than OWCTY_reversed. We experimented and compared the two algorithms using DiVinE, and confirmed improvements both in performance and scalability.

    KW - Accepting cycle search

    KW - Model checking

    KW - Parallelization

    KW - Strongly connected components

    UR - http://www.scopus.com/inward/record.url?scp=78650971028&partnerID=8YFLogxK

    UR - http://www.scopus.com/inward/citedby.url?scp=78650971028&partnerID=8YFLogxK

    U2 - 10.1527/tjsai.26.341

    DO - 10.1527/tjsai.26.341

    M3 - Article

    AN - SCOPUS:78650971028

    VL - 26

    SP - 341

    EP - 346

    JO - Transactions of the Japanese Society for Artificial Intelligence

    JF - Transactions of the Japanese Society for Artificial Intelligence

    SN - 1346-0714

    IS - 2

    ER -