安全なシステム構築のため，形式検証の重要性が増している．形式検証において，線形時間論理（LTL）はシステム動作仕様を厳密に記述するために広く用いられる．多くの検証法ではLTL式をオートマトンに変換するが，この変換はLTL式のサイズに対して指数オーダーであり，計算コストが高い．本研究では，代表的な変換手法であるタブロー法の効率化を目的とする．BDD（Binary Decision Diagram）を用いた既存手法があるが，ここではBDDとその変種であるZDDを組み合わせて利用する実装手法を提案する．実験を通じて，提案手法の有効性を確認する．