文献

J-GLOBAL ID：201402244694582697   整理番号：14A1010313

Hash Compactionを利用したグラフ書換え系モデル検査の大規模化とその評価

Evaluation of Large-scale Graph Rewriting Model Checking Using Hash Compaction

著者 (3件)： 吉田健人 (早稲田大 大学院基幹理工学研究科) ,  小沼賢 (早稲田大 大学院基幹理工学研究科) ,  上田和紀 (早稲田大 大学院基幹理工学研究科)
資料名： 電子情報通信学会技術研究報告  (IEICE Technical Report (Institute of Electronics, Information and Communication Engineers))
巻： 114  号： 156(DC2014 18-20)  ページ： 9-16  発行年： 2014年07月22日 
JST資料番号： S0532B  ISSN： 0913-5685  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： グラフ書換え系モデル検査とはグラフ書換え系をモデリング言語として,そのモデルが取りうる全ての状態を網羅的に探索することで,要求された性質を満たすか否かを判定する検証手法である。グラフ書換え系はモデルのもつ情報構造の表現力が高い。このことがモデル検査における状態数削減の効果をもたらすこともある。しかし,その半面時間・空間的に効率が悪いという欠点がある。本稿では,グラフ書換え系モデル検査においてHash Compactionを利用した空間・時間的改善手法をLMNtal並列モデル検査器SLIMに実装し,計測を行った。またHash Compactionは完全な状態空間の再現を保証しないので,ハッシュ関数の精度が状態空間に与える影響の考察と評価を行った。(著者抄録)

シソーラス用語： *技術 ,  数学モデル ,  ハッシュ関数 ,  モデル検査 ,  *項書換え系 ,  ハッシング ,  圧縮 ,  言語モデル ,  言語処理系 ,  *モデル検査技術
準シソーラス用語： Hash Compaction ,  LMNtal ,  SLIM ,  *グラフ書換え

分類 (1件)： その他の情報処理  (JE15050M)

引用文献 (18件)：

• Austin Appleby : murmurhash, 2009, https://sites.google.com/site/murmurhash/.
• Barnat, J., Brim, L., Cerna, I., Moravec, P., Rockai, P., Simecek, P. : DiVinE - A Tool for Distributed Verification, in Proc. CAV 2006, LNCS 4144, pp. 278-281, 2006.
• Barnat, J., Brim, L., Ročkai, P.: On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties, Science of Computer Programming, Vol. 77, No. 12, pp. 1272-1288, 2012.
• Barnat, J., Havlicek, J., Rockai, P.: Distributed LTL Model Checking with Hash Compaction, Electronic Notes in Theoretical Computer Science, Vol. 296, pp. 79-93, 2013.
• Brim, L., Cerna, I., Moravec, P., Simsa, J. : Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking, in Proc. FMCAD 2004, LNCS 3312, pp. 352-366, 2004.

タイトルに関連する用語 (5件)： グラフ ,  書換え系 ,  モデル検査 ,  大規模 ,  評価