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

  • Software
  • Artificial Intelligence

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

引用スタイル