Die in der Tabelle beschriebene temporale Logik wird CTL (Computeation Tree Logic) genannt. Sie geht auf einen Artikel von Clarke und Emerson aus dem Jahr 1981 zurück. Sie ergibt sich aus der booleschen Logik kombiniert mit vier temporalen Operatoren. Die vier Operatoren stehen für die Aussagen "im nächsten Taktschritt", "immer", "irgendwann" und "bis". Sie werden mit den Symbolen X, G, F und U abgekürzt. Die ersten drei temporalen Operatoren sind unär. Für die "bis"-Operation werden zwei Argumente benötigt. Der Einfachheit halber sind hier und im Folgenden bei den booleschen Funktionen nur "und", "oder" und "Negation" aufgeführt. Zusätzlich muss bestimmt werden, ob eine Bedingung auf einem Weg oder auf allen möglichen Wegen erfüllt sein muss. Dies wird durch zwei zusätzliche Pfadquantoren A und E geleistet. Eine vollständige CTL-Formel setzt sich aus jeweils einem Pfadquantor, einem temporalen Operator und einer bzw. zwei Argumentmengen zusammen.