Computation Tree Logic

temporale Logik mit Baumstruktur

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.

CTL-Formeln visualisiert

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.

Minimale Grammatik

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

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

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
  • 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