情報処理学会 第80回全国大会講演要旨

モデル検査というシステム正当性検証手法では、モデルサイズの増加に比してモデルの状態空間が爆発的に大きくなることが多い。状態空間の増加を緩和させる手段の一つとしてグラフ書換え系モデリング言語の使用が挙げられるが、『新規状態候補と同値な状態が状態空間内に存在するか』の判定を行う処理が検査時間のボトルネックになると考えられている。本研究では、同処理の効率化をめざすため、グラフの書換え差分をもとにグラフの書換え前後の正規形の差分を算出し、状態空間内のグラフ正規形の差分を利用してグラフ同型性判定を行う手法を導入し、評価を行った。