Computation Tree Logic – Wikipedia
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
[Bearbeiten | Quelltext bearbeiten]Minimale Grammatik
[Bearbeiten | Quelltext bearbeiten]Sei eine Menge von atomaren Aussagen (Behauptungen), dann ist jedes Element eine CTL-Formel. Sind und Formeln, dann auch , , , und . Dies definiert die minimale Grammatik von CTL. In der Regel wird diese allerdings um die gängigen booleschen Operatoren , und , sowie einigen weiteren temporalen Operatoren erweitert.
Temporale Operatoren
[Bearbeiten | Quelltext bearbeiten]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:
- – auf allen Pfaden folgt (englisch: All)
- – auf mindestens einem Pfad folgt (englisch: Exists)
- Pfad-spezifische Operatoren:
- – unmittelbar folgt (englisch: neXt state)
- – irgendwann folgt (englisch: some Future state oder Finally)
- – auf dem folgenden Pfad folgt in jedem Zustand (englisch: Globally)
- – folgt bis zum Erreichen des Zustands (englisch: Until)
- – 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:
- – in (mind.) einem nächsten Zustand gilt
- – in (mind.) einem der folgenden Zustände gilt
- – es gibt (mind.) einen Pfad, so dass entlang des ganzen Pfades gilt
- – es gibt einen Pfad, für den gilt: bis zum ersten Auftreten von gilt
- – in jedem nächsten Zustand gilt
- – man erreicht immer einen Zustand, in dem gilt
- – auf allen Pfaden gilt in jedem Zustand
- – es gilt immer bis zum ersten Auftreten von
Semantik
[Bearbeiten | Quelltext bearbeiten]CTL Formeln werden über Transitionssysteme definiert. Für eine gegebene Folge von Zuständen des Systems (beginnend in Zustand ) sind die Operatoren formal wie folgt definiert, dabei steht für erfüllt :
Die oben genannten Umformungen erlauben es, Formeln ineinander umzuwandeln.
Literatur
[Bearbeiten | Quelltext bearbeiten]- 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