形式仕様検証では，仕様をすべての入力パターンについて網羅的に解析し，問題となる入力パターンがあればそれを反例として導出する．このような反例入力パターンは欠陥の原因を探ることに活用できるが，その導出は高コストであることが欠点として挙げられる．本研究では，ωオートマトンによるリアクティブシステム仕様の反例入力パターンの効率的な導出を目的とし，新たな効率化手法を提案する．従来手法の多くはシンボリック技法によるものだったが，提案手法は明示的技法を基本として，反例探索において不必要なωオートマトンの遷移を除去するものである．実験を通し，この手法の有効性を確認する．