Computation Tree Logic - LinkFang.de





Computation Tree Logic


Die Computation Tree Logic (kurz CTL) ist eine Temporale Logik, die speziell zur Spezifikation und Verifikation von Computersystemen dient. Eine bestimmte Verallgemeinerung der unten beschriebenen Logik, für die der Name CTL steht, wird als CTL* bezeichnet. CTL bezeichnet dann eine spezielle Teilmenge der CTL*-Formeln. Eine weitere wichtige spezielle Teilmenge von CTL* ist die Linear Temporal Logic (kurz LTL).

Wie allgemein bei temporalen Logiken geht es nicht um die Beschreibung von zeitlichen Abläufen (dies wäre die Real Time Logic), sondern um die Eigenschaften von Zuständen und deren Änderung in Systemabläufen. LTL, CTL und CTL* sind dabei Erweiterungen der Aussagenlogik.

Syntax und Semantik

Atomare Aussagen

(siehe auch den Abschnitt "Umgangssprachliche Einleitung" im Artikel Aussagenlogik)

Ausgangspunkt sind Eigenschaften von Zuständen. Ist AP eine Menge von atomaren Aussagen (Behauptungen), so ist jedes Element p von AP eine Zustandsformel. Jedes p von AP ist eine Abbildung von der Zustandsmenge in die Menge der Wahrheitswerte {Wahr, Falsch}. Man sagt ein Zustand s erfüllt ein p aus AP genau dann, wenn [math]p(s)=W[/math].

Boolesche Operatoren

Aus den atomaren Formeln können nun aussagenlogische Formeln konstruiert werden. Durch den einstelligen Operator [math]\neg[/math] und die zweistelligen Operatoren [math]\wedge,\vee,\Rightarrow,\iff[/math], können wie bei der Aussagenlogik üblich neue Formeln im Sinne von NICHT, UND, ODER, IMPLIKATION und ÄQUIVALENZ gebildet werden.

Temporaloperatoren

Statt einzelner Zustände kann man nun unendliche Folgen solcher Zustände betrachten und darauf eine Semantik definieren. Die bisher definierten Formeln werden von einem Pfad erfüllt, wenn der erste Zustand des Pfades sie erfüllt. Diese Formeln werden nun durch die folgenden einstelligen Operationen erweitert:

  • X für den unmittelbar folgenden Zustand (englisch: neXt state)
  • F für einen irgendwann folgenden Zustand (englisch: some Future state)
  • G für alle folgenden Zustände (englisch: Globally)

Und die beiden zweistelligen Operatoren:

  • U für bis zum Erreichen des Zustands (englisch: Until)
  • R (englisch: Release)

Selten definiert man zusätzlich noch die Vergangenheitsformen:

  • P für vorheriger, (englisch: previous)
  • O für war einmal (englisch: once)
  • B für war immer (englisch: always been)
  • S für seit (englisch: since).

Pfade erfüllen diese Formeln nun genau dann, wenn (umgangssprachlich)

  1. ihr nächster Zustand [math]\phi[/math] erfüllt (X [math]\phi[/math]),
  2. irgendein Folgezustand [math]\phi[/math] erfüllt (F [math]\phi[/math]),
  3. alle Zustände [math]\phi[/math] erfüllen (G [math]\phi[/math]),
  4. [math]\phi[/math] gilt, bis ein Folgezustand erreicht wird, an dem [math]\psi[/math] erfüllt ist ([math]\phi[/math] U [math]\psi[/math]),
  5. [math]\psi[/math] gilt bis (einschließlich) zu dem Zustand, an dem [math]\phi[/math] erfüllt ist ([math]\phi[/math] R [math]\psi[/math]).

Für eine gegebene Folge von Zuständen [math]x_0, x_1, x_2, \ldots[/math] sind die Operatoren formal wie folgt definiert:

  1. [math]X\phi[/math] : = [math]x_1[/math] erfüllt [math]\phi[/math],
  2. [math]F\phi[/math] : = [math]\exists i\in \N: x_i[/math] erfüllt [math]\phi[/math],
  3. [math]G\phi[/math] : = [math]\forall i\in \N: x_i[/math] erfüllt [math]\phi[/math],
  4. [math]\phi U \psi[/math] : = [math]\exists i\in \N \quad \forall j \in \{a:a \in \N \land 0 \leq a \leq i\}: x_j [/math] erfüllt [math]\phi \land x_i [/math] erfüllt [math]\psi [/math],
  5. [math]\phi R \psi[/math] : = [math]\exist i\in \N \quad \forall j \in \{a:a \in \N \land 0 \leq a \leq i \} \quad \forall k \in \{a:a \in \N \land i \lt a \}: \psi[/math] erfüllt [math]x_j \land \phi[/math] erfüllt [math]x_k[/math]

Für F, G und U gilt die Prämisse "Zukunft schließt Gegenwart mit ein", d.h. wird eine Formel in einem der folgenden Zustände erfüllt, so gilt das auch für den Startzustand. Die bis hier definierten Formeln bilden die sogenannten Pfadformeln und die schon oben erwähnte Linear Time Temporal Logic.

Pfadquantoren

Statt Pfaden können auch Bäume von Zuständen betrachtet werden, die in jedem Zweig unendlich tief sind. Zu einer Pfadformel kann man mit den Quantoren E für entlang (mindestens) eines Pfades (englisch: exists) und A für entlang aller Pfade (englisch: always) Zustandsformeln gewinnen. Ein Baum erfüllt E [math]\phi[/math] genau dann, wenn es in diesem beginnend bei der Wurzel einen Pfad gibt, der [math]\phi[/math] erfüllt. Ein Baum erfüllt A [math]\phi[/math] genau dann, wenn jeder bei der Wurzel beginnende Pfad [math]\phi[/math] erfüllt.

Die so definierte Logik bildet nun CTL*.

Die Teilmenge CTL

Zu dieser Logik kann man noch eine Teilmenge definieren, die man wie schon oben erwähnt CTL nennt. Diese entstehen, wenn jeder Temporaloperator durch genau einen Pfadquantor quantifiziert wird. CTL wird also aus den atomaren Zustandsaussagen, den booleschen Operatoren und Paaren von Pfadquantor und Temporaloperator (in dieser Reihenfolge) gebildet. Die Aussagenlogik wird also um die Operatoren erweitert:

  • EX [math]\phi[/math] (in (mind.) einem nächsten Zustand gilt [math]\phi[/math]),
  • EF [math]\phi[/math] (in (mind.) einem der folgenden Zustände gilt [math]\phi[/math]),
  • EG [math]\phi[/math] (es gibt (mind.) einen Pfad, so dass [math]\phi[/math] entlang des ganzen Pfades gilt),
  • E[[math]\phi[/math] U [math]\psi[/math]] (es gibt einen Pfad für den gilt: bis zum ersten Auftreten von [math]\psi[/math] gilt [math]\phi[/math]),
  • AX [math]\phi[/math] (in jedem nächsten Zustand gilt [math]\phi[/math]),
  • AF [math]\phi[/math] (man erreicht immer einen Zustand, der [math]\phi[/math] erfüllt),
  • AG [math]\phi[/math] (auf allen Pfaden gilt in jedem Zustand [math]\phi[/math]) und
  • A[[math]\phi[/math] U [math]\psi[/math]] (es gilt immer [math]\phi[/math] bis zum ersten Auftreten von [math]\psi[/math]).

Sollen diese Operatoren als Ausgangspunkt für eine Fixpunktbestimmung genutzt werden, so genügt es die Zahl der Operatoren durch Umformungen auf diese drei zu begrenzen:

  • [math]EX \phi[/math]
  • [math]EG \phi[/math]
  • [math] E \phi U \psi[/math]

Dies ist der Fall, weil folgende Äquivalenzen gelten:

  • [math] AX \phi \equiv \neg EX (\neg \phi)[/math]
  • [math] EF \phi \equiv E ((true) U \phi)[/math]
  • [math] AG \phi \equiv \neg EF \neg \phi[/math]
  • [math] AF \phi \equiv \neg EG \neg \phi[/math]
  • [math] A (\phi U \psi) \equiv \neg E (\neg \psi U (\neg \phi \wedge \neg \psi)) \wedge \neg EG \neg \psi[/math]
  • [math] A (\phi R \psi) \equiv \neg E (\neg \phi U \neg \psi)[/math]
  • [math] E (\phi R \psi) \equiv \neg A (\neg \phi U \neg \psi)[/math]

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 1-402-07293-7
  • B. Berard, Michel Bidoit, Alain Finkel: Systems and Software Verification. Model-Checking Techniques and Tools.: 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

Kategorien: Mathematische Logik

Quelle: Wikipedia - http://de.wikipedia.org/wiki/Computation Tree Logic (Vollständige Liste der Autoren des Textes [Versionsgeschichte])    Lizenz: CC-by-sa-3.0

Änderungen: Alle Bilder mit den meisten Bildunterschriften wurden entfernt. Ebenso alle zu nicht-existierenden Artikeln/Kategorien gehenden internen Wikipedia-Links (Bsp. Portal-Links, Redlinks, Bearbeiten-Links). Entfernung von Navigationsframes, Geo & Normdaten, Mediadateien, gesprochene Versionen, z.T. ID&Class-Namen, Style von Div-Containern, Metadaten, Vorlagen, wie lesenwerte Artikel. Ansonsten sind keine Inhaltsänderungen vorgenommen worden. Weiterhin kann es durch die maschinelle Bearbeitung des Inhalts zu Fehlern gerade in der Darstellung kommen. Darum würden wir jeden Besucher unserer Seite darum bitten uns diese Fehler über den Support mittels einer Nachricht mit Link zu melden. Vielen Dank!

Stand der Informationen: August 201& - Wichtiger Hinweis: Da die Inhalte maschinell von Wikipedia übernommen wurden, ist eine manuelle Überprüfung nicht möglich. Somit garantiert LinkFang.de nicht die Richtigkeit und Aktualität der übernommenen Inhalte. Sollten die Informationen mittlerweile fehlerhaft sein, bitten wir Sie darum uns per Support oder E-Mail zu kontaktieren. Wir werden uns dann innerhalb von spätestens 10 Tagen um Ihr Anliegen kümmern. Auch ohne Anliegen erfolgt mindestens alle drei Monate ein Update der gesamten Inhalte.