Begriff
Computation Tree Logic (CTL)
Warum wichtig?
Dieser Begriff ist ein Knoten im SengakujiWorks-Wissensnetz. Nutze Level 0 für die erste Einordnung, Level 1 für Praxis, Level 2 für technische Struktur und Level 3 für Grenzen, Fallstricke und Expertenkontext.
LTL sagt: "Auf allen Pfaden passiert X." Was, wenn du sagen willst: "Es gibt einen Weg, das Spiel zu gewinnen"? (Es muss nicht jeder Weg gewinnen, das wäre langweilig). Oder: "Ich kann den Reaktor immer neustarten (egal was passiert)." (Reset-Möglichkeit). Dafür brauchst du Verzweigungen (Branches). CTL sieht die Zeit als Baum. Von jedem Punkt aus gehen viele Zukünfte ab. Wir quantifizieren über die Pfade:
- A (All): Auf allen abzweigenden Pfaden.
- E (Exists): Auf mindestens einem abzweigenden Pfad.
Merksatz: Eine verzweigte Temporallogik, die es ermöglicht, Aussagen über mögliche Zukünfte (Existenzquantoren) und notwendige Zukünfte (Allquantoren) in einem Berechnungsbaum zu treffen.
Kombination von Pfad-Quantoren (A, E) und Zeit-Operatoren (G, F, X).
- AG (Safe): Egal was ich tue, es ist immer sicher. (Safety).
- EF (Win): Es gibt einen Weg (Exists), irgendwann (Future) zu gewinnen. (Possibility).
- AF (Start): Egal welchen Weg ich wähle, irgendwann startet es. (Liveness).
- AGEF (Reset): Egal wo ich bin (AG), ich finde immer einen Weg zurück zum Start (EF Start). (Restartability).
1. Vergleich mit LTL
CTL kann "Reset" (AGEF) ausdrücken. LTL nicht.
LTL kann "Fairness" (GF P -> GF Q) ausdrücken. CTL nicht (oder nur sehr umständlich).
Deshalb gibt es CTL* (CTL Star), das beides vereint. (Aber extrem rechenintensiv ist).
2. NuSMV
Der bekannteste Model Checker für CTL. Er nutzt BDDs (Binary Decision Diagrams), um den riesigen Baum effizient zu speichern.
1. Branching Time vs. Linear Time
Der philosophische und mathematische Kern von CTL ist die Sicht auf die Zeit. In LTL ist die Zeit eine einzige Sequenz von Zuständen. In CTL ist sie ein Baum, bei dem jeder Knoten die "Eigenschaft" hat, bestimmte Zukünfte zu ermöglichen. Ein wichtiger Unterschied ist die Entscheidbarkeit. Während LTL-Model-Checking in der Größe der Formel exponentiell ist ($2^{|f|}$), ist CTL-Model-Checking linear in der Größe der Formel UND der Größe des Zustandsraums ($O(|f| \times (|S| + |R|))$). Warum nutzt man dann nicht nur CTL? Weil LTL Eigenschaften wie "Starke Fairness" ausdrücken kann, die in CTL (ohne Erweiterungen) nicht formulierbar sind.
2. Fairness-Constraints
In der Produktion (z.B. Protokoll-Verifikation) nimmt man oft an, dass ein Prozess irgendwann dran kommt, wenn er bereit ist. Das nennt man Fairness.
Reines CTL kann Fairness nicht direkt in der Formel ausdrücken. Model Checker wie NuSMV erlauben es daher, zusätzliche FAIRNESS-Keywords anzugeben. Der Model Checker filtert dann alle Pfade im Baum heraus, die "unfair" sind (z.B. ein Prozess, der ewig hungert). Nur auf den verbleibenden "fairen" Zweigen wird die CTL-Formel geprüft.
3. Symbolic Model Checking & BDDs
Früher war Model Checking auf 10.000 Zustände begrenzt.
Ken McMillan revolutionierte das Feld, indem er CTL-Eigenschaften auf BDDs (Binary Decision Diagrams) prüfte.
Anstatt jeden Zustand einzeln zu besuchen, wird die gesamte Menge der Zustände, in denen eine Eigenschaft (z.B. EF Win) gilt, als boolesche Funktion dargestellt. Man berechnet Fixpunkte über Mengen von Zuständen. Das ermöglichte es erstmals, Systeme mit $10^{20}$ Zuständen und mehr zu verifizieren, was den Weg für den Einsatz bei Intel und IBM ebnete.
Quick-Check
Was ist besser?
Geschmacksfrage. Hardware-Designer (Intel) lieben CTL. Software-Leute lieben LTL (intuitiver für Algorithmen).Warum Baum?
Weil Computer "nicht-deterministisch" sind (User-Input, Interrupts). Jeder Input ist eine Astgabelung.Ist E X P das Gleiche wie X P?
In LTL gibt es kein E. In CTL heißtEX P: "Es gibt einen Next Step, wo P wahr ist." Das ist wichtig. Wenn ich in einer Sackgasse (Deadlock) bin, istAX Pwahr (Trivial), aberEX Pfalsch (Kein Nachfolger).