Für einfache Bedingungen in digitalen Systemen ist die boolesche Logik ausreichend. Beispielsweise könnte y = x1x2 eine zu überprüfende Spezifikationsbedingung sein. Bei genauerer Betrachtung fällt auf, dass für sequenzielle Systeme eine solche Bedingung eine unvollständige Beschreibung liefert. Soll diese Bedingung immer gelten oder ist es ausreichend, dass y = x1x2 irgendwann einmal gilt? Das heißt, für eine genauere Beschreibung sind zeitliche Zusammenhänge mit zu spezifizieren.
Dies kann durch temporale Logiken geschehen, in denen der Wahrheitsgehalt einer Funktion von der Zeit abhängt. Temporale Logiken werden in die beiden Klassen lineare temporale Logik (Linear Time Logic) und verzweigende temporale Logik (Branching Time Logic) eingeteilt. Bei den linearen temporalen Logiken geht man davon aus, dass das Systemverhalten in der Zukunft eindeutig bestimmt ist, dass es also keine verschiedenen Entwicklungen in der Zukunft geben kann. Dagegen lässt das verzweigende Zeitmodell in der Zukunft verschiedene Entwicklungen zu, die durch nichtdeterministisches Verhalten des Systems oder durch unterschiedliche Eingangsgrößen hervorgerufen werden können.
Bei dem verzweigenden Zeitmodell besteht die zeitliche Entwicklung nicht aus einer linearen Sequenz von Zuständen, sondern die Systemzustände fächern sich in der Zukunft auf. Es entsteht ein Baum, dessen Wurzel der momentane Systemzustand ist.
Demnach können zu einem Zeitpunkt in der Zukunft verschiedene Systemzustände existieren. Welchen Weg das System einschlagen wird, ist für die Betrachtung irrelevant, da alle Wege gleichberechtigt betrachtet werden, um eine allgemeingültige Aussage zu erhalten.