人工知能学会論文誌
Online ISSN : 1346-8030
Print ISSN : 1346-0714
ISSN-L : 1346-0714
速報論文
LMNtal並列モデル検査における状態生成数削減及び高速化
安田 竜吉田 健人上田 和紀
著者情報
ジャーナル フリー

2014 年 29 巻 1 号 p. 182-187

詳細
抄録
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.
引用文献 (14)
著者関連情報
© 人工知能学会 2014
前の記事 次の記事
feedback
Top