モデル検査技法は，仕様に対する設計の妥当性検証への適用において，近年大きな成功をおさめている．この技法の適用範囲をさらに広げるためには，状態数爆発問題を解決することが必要である．この問題を解決する方法として注目されている抽象化技法，およびそれを実装したツールを紹介する．