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

Ryo Yasuda, Taketo Yoshida, Kazunori Ueda

    Research output: Contribution to journalArticle

    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.

    Original languageEnglish
    Pages (from-to)182-187
    Number of pages6
    JournalTransactions of the Japanese Society for Artificial Intelligence
    Volume29
    Issue number1
    DOIs
    Publication statusPublished - 2014

    Fingerprint

    Model checking
    Computer programming languages
    Scalability

    Keywords

    • Accepting cycle search
    • Model checking
    • Nested depth first search
    • Parallelization

    ASJC Scopus subject areas

    • Artificial Intelligence
    • Software

    Cite this

    Reduction of the number of states and the acceleration of LMNtal parallel model checking. / Yasuda, Ryo; Yoshida, Taketo; Ueda, Kazunori.

    In: Transactions of the Japanese Society for Artificial Intelligence, Vol. 29, No. 1, 2014, p. 182-187.

    Research output: Contribution to journalArticle

    @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 -