Computation Tree Logic

Die Computation Tree Logic (kurz CTL) ist eine temporale Logik, deren Modell der Zeit eine baumartige Struktur hat. Die zeitliche Änderung von Zuständen und deren Eigenschaften wird durch Pfade innerhalb dieser Baumstruktur modelliert. Hierbei hat die Zukunft mehrere Pfade, wobei nicht festgelegt ist, welche letztendlich realisiert werden. Demnach können Aussagen über die mögliche Entwicklungen getroffen werden.

Die CTL wird zur Verifikation von Hard- und Software verwendet, üblicherweise von Model Checkern.

Zu der Familie der temporalen Logiken gehört auch die linear temporale Logik (LTL), wobei hier nur eine Zukunft möglich ist. Eine Verallgemeinerung der beiden Logiken wird als CTL* bezeichnet.

Syntax

Minimale Grammatik

Sei $A P$ eine Menge von atomaren Aussagen (Behauptungen), dann ist jedes Element $p \in A P$ eine CTL-Formel. Sind $ϕ$ und $ψ$ Formeln, dann auch $\neg ϕ$ , $ϕ \lor ψ$ , $EX ϕ$ , $EG ϕ$ und $ϕ EU ψ$ . Dies definiert die minimale Grammatik von CTL. In der Regel wird diese allerdings um die gängigen booleschen Operatoren $\land$ , $⟹$ und $\Leftrightarrow$ , sowie einigen weiteren temporalen Operatoren erweitert.

Temporale Operatoren

Die Erweiterung der minimalen Grammatik um folgende Operatoren erhöht nicht die Mächtigkeit der Sprache, da alle Operatoren durch Umformungen zurückgeführt werden können.

Pfadoperatoren:
- $A ϕ$ – auf allen Pfaden folgt $ϕ$ (englisch: All)
- $E ϕ$ – auf mindestens einem Pfad folgt $ϕ$ (englisch: Exists)
Pfad-spezifische Operatoren:
- $X ϕ$ – unmittelbar folgt $ϕ$ (englisch: neXt state)
- $F ϕ$ – irgendwann folgt $ϕ$ (englisch: some Future state oder Finally)
- $G ϕ$ – auf dem folgenden Pfad folgt in jedem Zustand $ϕ$ (englisch: Globally)
- $ϕ U ψ$ – $ϕ$ folgt bis zum Erreichen des Zustands $ψ$ (englisch: Until)
- $ϕ W ψ$ – $ϕ$ folgt immer oder bis zum Erreichen des Zustands $ψ$ (englisch: Weak Until)

Pfad und pfad-spezifische Operatoren können miteinander kombiniert werden, sodass sich beispielsweise folgende Formeln ergeben:

$E X ϕ$ – in (mind.) einem nächsten Zustand gilt $ϕ$
$E F ϕ$ – in (mind.) einem der folgenden Zustände gilt $ϕ$
$E G ϕ$ – es gibt (mind.) einen Pfad, so dass $ϕ$ entlang des ganzen Pfades gilt
$E [ϕ U ψ]$ – es gibt einen Pfad, für den gilt: bis zum ersten Auftreten von $ψ$ gilt $ϕ$
$A X ϕ$ – in jedem nächsten Zustand gilt $ϕ$
$A F ϕ$ – man erreicht immer einen Zustand, in dem $ϕ$ gilt
$A G ϕ$ – auf allen Pfaden gilt in jedem Zustand $ϕ$
$A [ϕ U ψ]$ – es gilt immer $ϕ$ bis zum ersten Auftreten von $ψ$

Semantik

CTL Formeln werden über Transitionssysteme definiert. Für eine gegebene Folge von Zuständen des Systems $T (s_{0}) = s_{0}, s_{1}, \dots$ (beginnend in Zustand $s_{0}$ ) sind die Operatoren formal wie folgt definiert, dabei steht $T (s_{0}) ⊨ ϕ$ für $T (s_{0})$ erfüllt $ϕ$ :

$T (s_{0}) ⊨ \neg ϕ \Leftrightarrow T (s_{0}) ⊭ ϕ$
$T (s_{0}) ⊨ ϕ \lor ψ \Leftrightarrow T (s_{0}) ⊨ ϕ oder T (s_{0}) ⊨ ψ$
$T (s_{0}) ⊨ E X ϕ \Leftrightarrow T (s_{1}) ⊨ ϕ$
$T (s_{0}) ⊨ E G ϕ \Leftrightarrow \forall i : T (s_{i}) ⊨ ϕ$
$T (s_{0}) ⊨ ϕ E U ψ \Leftrightarrow \exists k : T (s_{k}) ⊨ ψ \land \forall i < k : T (s_{i}) ⊨ ϕ$

Die oben genannten Umformungen erlauben es, Formeln ineinander umzuwandeln.

$\neg A ϕ \equiv E \neg ϕ$
$\neg A F ϕ \equiv E G \neg ϕ$
$\neg E F ϕ \equiv A G \neg ϕ$
$\neg A X ϕ \equiv E X \neg ϕ$
$A G ϕ \equiv ϕ \land A X A G ϕ$
$E G ϕ \equiv ϕ \land E X E G ϕ$
$A F ϕ \equiv ϕ \lor A X A F ϕ$
$E F ϕ \equiv ϕ \lor E X E F ϕ$
$A [ϕ U ψ] \equiv ψ \lor (ϕ \land A X A [ϕ U ψ])$
$E [ϕ U ψ] \equiv ψ \lor (ϕ \land E X E [ϕ U ψ])$

Literatur

Clarke, Grumberg, Peled: Model Checking. MIT Press, 2000, ISBN 0-262-03270-8
Rohit Kapur: CTL for Test Information of Digital ICS. Springer, 2002, ISBN 978-1-4020-7293-2
B. Berard, Michel Bidoit, Alain Finkel: Systems and Software Verification. Model-checking Techniques and Tools. Springer, 2001, ISBN 3-540-41523-8
M. Huth and M. Ryan: Logic in Computer Science - Modelling and Reasoning about Systems. Cambridge, 2004, ISBN 0-521-54310-X