Binary Decision Diagram。モデル検査法の代表的なアルゴリズムの1つで、論理関数を0と1のグラフで表現し、全探索を行う方法です。全探索を基本的に行うため、論理関数の構成によっては、状態爆発が発生することが多いです。SCADEのモデル検査アルゴリズムでは、二分決定グラフ（BDD）を使用していません。