Reduction of the number of states and the acceleration of LMNtal parallel model checking

Ryo Yasuda, Taketo Yoshida, Kazunori Ueda

    研究成果: Article

    抄録

    SLIM is an LMNtal runtime. LMNtal is a programming and modeling language based on hierarchical graph rewriting. SLIM features automata-based LTL model checking that is one of the methods to solve accepting cycle search problems. Parallel search algorithms OWCTY and MAP used by SLIM generate a large number of states for problems having and accepting cycles. Moreover, they have a problem that performance seriously falls for particular problems. We propose a new algorithm that combines MAP and Nested DFS to remove states for problems including accepting cycles. We experimented the algorithm and confirmed improvements both in performance and scalability.

    元の言語English
    ページ(範囲)182-187
    ページ数6
    ジャーナルTransactions of the Japanese Society for Artificial Intelligence
    29
    発行部数1
    DOI
    出版物ステータスPublished - 2014

    Fingerprint

    Model checking
    Computer programming languages
    Scalability

    ASJC Scopus subject areas

    • Artificial Intelligence
    • Software

    これを引用

    @article{2415998628364ab591031ec3e2d31802,
    title = "Reduction of the number of states and the acceleration of LMNtal parallel model checking",
    abstract = "SLIM is an LMNtal runtime. LMNtal is a programming and modeling language based on hierarchical graph rewriting. SLIM features automata-based LTL model checking that is one of the methods to solve accepting cycle search problems. Parallel search algorithms OWCTY and MAP used by SLIM generate a large number of states for problems having and accepting cycles. Moreover, they have a problem that performance seriously falls for particular problems. We propose a new algorithm that combines MAP and Nested DFS to remove states for problems including accepting cycles. We experimented the algorithm and confirmed improvements both in performance and scalability.",
    keywords = "Accepting cycle search, Model checking, Nested depth first search, Parallelization",
    author = "Ryo Yasuda and Taketo Yoshida and Kazunori Ueda",
    year = "2014",
    doi = "10.1527/tjsai.29.182",
    language = "English",
    volume = "29",
    pages = "182--187",
    journal = "Transactions of the Japanese Society for Artificial Intelligence",
    issn = "1346-0714",
    publisher = "Japanese Society for Artificial Intelligence",
    number = "1",

    }

    TY - JOUR

    T1 - Reduction of the number of states and the acceleration of LMNtal parallel model checking

    AU - Yasuda, Ryo

    AU - Yoshida, Taketo

    AU - Ueda, Kazunori

    PY - 2014

    Y1 - 2014

    N2 - SLIM is an LMNtal runtime. LMNtal is a programming and modeling language based on hierarchical graph rewriting. SLIM features automata-based LTL model checking that is one of the methods to solve accepting cycle search problems. Parallel search algorithms OWCTY and MAP used by SLIM generate a large number of states for problems having and accepting cycles. Moreover, they have a problem that performance seriously falls for particular problems. We propose a new algorithm that combines MAP and Nested DFS to remove states for problems including accepting cycles. We experimented the algorithm and confirmed improvements both in performance and scalability.

    AB - SLIM is an LMNtal runtime. LMNtal is a programming and modeling language based on hierarchical graph rewriting. SLIM features automata-based LTL model checking that is one of the methods to solve accepting cycle search problems. Parallel search algorithms OWCTY and MAP used by SLIM generate a large number of states for problems having and accepting cycles. Moreover, they have a problem that performance seriously falls for particular problems. We propose a new algorithm that combines MAP and Nested DFS to remove states for problems including accepting cycles. We experimented the algorithm and confirmed improvements both in performance and scalability.

    KW - Accepting cycle search

    KW - Model checking

    KW - Nested depth first search

    KW - Parallelization

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

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

    U2 - 10.1527/tjsai.29.182

    DO - 10.1527/tjsai.29.182

    M3 - Article

    AN - SCOPUS:84940317075

    VL - 29

    SP - 182

    EP - 187

    JO - Transactions of the Japanese Society for Artificial Intelligence

    JF - Transactions of the Japanese Society for Artificial Intelligence

    SN - 1346-0714

    IS - 1

    ER -