[2N6-GS-1] 基礎・理論: 制約充足と最適化

[2N6-GS-1-01] グラフ書き換えモデル検査におけるグラフ自己同型に基づく効率的なSymmetry Reduction手法

〇恒川 雄太郎¹、上田 和紀² (1. 早稲田大学大学院基幹理工学研究科、2. 早稲田大学理工学術院情報理工学科)

キーワード：モデル検査、グラフ書換え系、状態空間探索

モデル検査においてモデルのサイズに対して状態数が爆発的に増加する問題は重要な課題である．
Symmetry Reductionとは状態の対称性に着目した探索空間削減手法である．
グラフ書き換えに基づくモデル検査器SLIMは，グラフ構造の対称性を用いてSymmetry Reductionを行うことで探索空間を削減しているが，その際に頻発するグラフ同型生判定が実行時間性能のボトルネックになっている．
本研究では探索中にグラフの自己同型性を用いてグラフ同型性判定の回数を削減することで，効率的なSymmetry Reductionを実現する手法を提案する．本手法はグラフ中の自己同型な部分に対する書き換え結果は状態空間中で必ず対称な状態になることに注目し，グラフ同型性判定の回数を削減する．本手法をモデル検査器SLIMに実装し，対称性の高いモデルに対してグラフ同型性判定回数のオーダーが減少したことを確認した．