リアクティブシステムの仕様の安全性を確かめるために数学的技法を用いた形式検証に注目が集まっている．形式検証を用いて仕様に欠陥が存在するか判定できる．もし欠陥があれば，仕様を修正しなくてはならない．修正には，判定で得られる反例が利用される．その際に反例は単純な方が効率的に修正を行える．しかし，既存の反例導出ツールでは必ずしも単純な反例が導出されるとは限らない．本研究では，理解のしやすさ向上と機械的な修正サポートの効率化のための単純な反例を導出する手法の提案とその実装を行う．仕様から全ての反例を表現する無限木オートマトンを構成し，SATソルバを用いて解析していくことで単純な反例を導出する．