Da bei sequentiellen Schaltungen (Automaten) sehr viele Zustände auftreten können, mussten Methoden gefunden werden, über Zustandsmengen mit einer großen Kardinalität zu argumentieren. Ein Durchbruch dazu war das Symbolic Model Checking. Im Wesentlichen werden dazu Beschreibungen für Zustandsmengen und Zustandsübergangsrelationen benötigt. Im Folgenden wird eine Speicherung dieser Daten mithilfe von charakterischen Funktionen erläutert.
Betrachtet man alle Wertebelegungen des Variablenvektors z einer Booleschen Funktion fA, bei der das Ergebnis der Funktion 1 entspricht, so ergibt sich eine Menge von Werten A = {z | fA(z) = 1}. Identifiziert man einen Zustand eines Zustandsautomaten mit jeweils einem dieser Vektoren, können Zustandsmengen durch boolesche Funktionen und damit auch mit OBDDs beschrieben werden. Die boolesche Funktion fA(z) wird als charakteristische Funktion der Wertemenge A bezeichnet.
fA(z) = 1, falls z Element von A oder 0, falls nicht
Zur Beschreibung von Zustandsübergängen muss die Darstellung erweitert werden. Für jeden Zustand z1 bestimmt man einen oder mehrere Folgezustände z2. Das heißt, die Zustandsübergangs-Relation kann beispielsweise als delta(z1,z2) beschrieben werden. Damit können Algorithmen symbolisch über Millionen von Zuständen und deren sequentielle Abarbeitung argumentieren, ohne diese explizit aufzählen zu müssen.