リアクティブシステム仕様の実現可能性判定に関する検証は，仕様から等価な無限木オートマトンを構成し，それを分析することで行われる．これによりシステムの高信頼化を可能とするが，検証にかかるコストは極めて高い．本研究では，実現可能性判定コスト削減のため，構成した無限木オートマトンに局所情報の捨象を適用する分割検証法を提案する．複数のモジュールに分割した仕様から無限木オートマトンを構成し，分割先でのみ現れる局所情報の捨象を適用したものを統合，分析する手法を与えることで効率を向上させる．評価実験で一括検証と提案手法との効率の比較を行い，提案手法の有効性を確認する．