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.