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

      フィンガープリント

    ASJC Scopus subject areas

    • Artificial Intelligence
    • Software

    これを引用