Computation Tree Logic

Die Computation Tree Logic (kurz CTL) ist eine spezielle Temporale Logik, die speziell zur Spezifikation und Verifikation von Computersystem dient. Meißt wird sie auch mit CTL* bezeichnt. CTL bezeichnet dann einge spezielle Teilmenge der CTL*-Formeln. Eine weitere wichtige spezielle Teilmenge von CTL* ist LTL.

Wie allgemein bei temporalen Logiken geht es nicht um die Beschreibung von zeitlichen Abläufen (dies wäre die Real Time Logik), sondern um die Eigenschaften von Zuständen und deren Änderung in Systemabläufen. CTL* ist dabei eine Erweiterung der Aussagenlogik.

Syntax und Semantik

Atomare Aussagen

Ausganspunkt sind Eigenschaften von Zuständen. Ist AP eine Menge von atomaren Aussagen, so ist jedes Element p von AP eine Zustansformel in AP. Jedes p von AP ist eine Abbildung von der Zustandsmenge in die Menge der Wahrheitswerte {W,F}. Man sagt ein Zustand s erfüllt ein p aus AP genau dann, wenn p(s)=W.

Aussagenlogische Formeln

Aus den atomaren Formeln können nun aussagenlogische Formeln konstruhiert werden. Durch die Operatoren Fehler beim Parsen (Unbekannte Funktion „\we“): {\displaystyle \wedge,\we,\not,\Reightarrow.\iff}