6L-06
クリプキ構造に着目した機械学習に基づくモデル検査の評価
○福地恵大,岸 知二(早大)
モデル検査とは,仕様記述と性質記述を与えたとき,そのモデル上で記述された性質が成立するか検証する手法である.モデル検査はモデルを全数探索する技術であり,状態数が大きくなると現実的な時間やメモリ量で検査が終了しない状態爆発が起こりうる.状態爆発への対応として,機械学習を用いてモデル検査の結果を予測する研究が行われている.本研究では,クリプキ構造に着目して,機械学習アルゴリズムによるモデル検査の結果予測精度を評価する.