/ プログラム/ 発表一覧/ 著者一覧/ 企業展示一覧/ jsai2013ホーム /

1B5-6 LMNtal 並列モデル検査における 状態生成数削減及び高速化

*セッションの無断動画配信はご遠慮下さい。

Tweet #jsai2013 このエントリーをはてなブックマークに追加

06月04日(Tue) 18:40〜20:20 B会場(-国際会議場201号室)
1B5 基礎・理論「基礎・理論-1」

演題番号1B5-6
題目LMNtal 並列モデル検査における 状態生成数削減及び高速化
著者安田 竜(早稲田大学基幹理工学部情報理工学科)
上田 和紀(早稲田大学理工学術院情報理工学科)
吉田 健人(早稲田大学基幹理工学部情報理工学科)
時間06月04日(Tue) 20:00〜20:20
概要階層グラフ書き換え言語LMNtalの実行時処理系であるSLIMには,プログラムの検証を行うモデル検査機能が実装されている.SLIMで採用されているMAP,OWCTY等の並列探索アルゴリズムは、エラーを含む問題に対して状態生成数が多くなるほか,特定の問題に対して極端に性能が落ちるという問題を抱えている.本研究では,これらの問題を解決するため,新たなアルゴリズムの設計と実装を行い,その性能を評価した.
論文PDFファイル