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

    フィンガープリント 「Reduction of the number of states and the acceleration of LMNtal parallel model checking」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

    引用スタイル