Lineare temporale Logik

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche

Lineare temporale Logik (LTL oder Linear temporal logic) ist ein Modell temporaler Logik mit zeitlichen Modalitäten. In LTL können Formeln über die Zukunft von Pfaden aufgestellt werden, beispielsweise dass eine Bedingung irgendwann wahr wird oder eine Bedingung wahr bleibt, bis eine andere Bedingung erfüllt wird.

Syntax[Bearbeiten]

LTL ist aus einer Menge von Aussagenvariablen p_1, p_2, ..., den logischen Verknüpfungen \neg,\or,\and,\rightarrow und den nachfolgenden temporalen modalen Operatoren aufgebaut:

  • X für Nachfolger (next; N wird synonym benutzt)
  • G für global
  • F für irgendwann (finally)
  • U für bis (until)
  • R für Auflösung (release).

Die ersten drei Operatoren sind unär, so dass X \phi eine syntaktisch korrekte Formel ist, wenn \phi syntaktisch korrekt ist. Die letzten zwei Operatoren sind binär, so dass \phi U \psi eine syntaktisch korrekte Formel ist, wenn \phi und \psi syntaktisch korrekte Formeln sind.

Semantik[Bearbeiten]

Eine LTL-Formel kann sowohl über einer unendlichen Sequenz von Aussagen als auch einer einzigen Position auf dem Pfad ausgewertet werden. Eine LTL-Formel ist genau dann auf einem Pfad erfüllt, wenn sie auf Position 0 des Pfades erfüllt ist. Die Semantik der modalen Operatoren ist wie folgt.

Textform Symbol Erklärung Beispielpfad
Einstellige Verknüpfungen:
X \phi \circ \phi nächster (NeXt): \phi gilt am nächsten Zustand. Ltlnext.png
G \phi \Box \phi Global: \phi gilt auf dem kompletten nachfolgenden Pfad. Ltlalways.png
F \phi \Diamond \phi Finally: \phi gilt irgendwann auf dem nachfolgenden Pfad. Ltlevently.png
Zweistellige Verknüpfungen:
\psi U \phi \psi\mathcal{U}\phi Until: \phi gilt an der aktuellen oder einer nachfolgenden Position und \psi gilt solange bis diese Position erreicht ist. An dieser Position muss \psi nicht mehr gelten. Ltluntil.png
\psi R \phi \psi\mathcal{R}\phi Release: \phi gilt einschließlich bis zur ersten Position, an der \psi gilt oder für immer, wenn eine solche Position nicht existiert. Ltlrelease1.png

Ltlrelease2.png

Bereits zwei der Operatoren sind fundamental, das heißt sie definieren die anderen durch geeignete Verknüpfungen:

  • F \phi = true U \phi
  • G \phi = false R \phi = \neg F \neg\phi
  • \psi R \phi = \neg(\neg\psi U \neg\phi)

Sonderverknüpfungen[Bearbeiten]

Einige Autoren definieren einen schwachen bis-Operator (weak until, mit W bezeichnet), der eine ähnliche Semantik wie der bis-Operator besitzt, jedoch keine Haltebedingung erforderlich ist. Manchmal ist es sinnvoll, wenn U und R mit Formeln des schwachen bis-Operators definiert werden können:

  • \psi U \phi = F \phi\land(\psi W \phi)
  • \psi R \phi = \phi W (\psi\land\phi)
  • \phi W \psi = \psi R (\psi\lor\phi)
  • \phi W \psi = (\phi U \psi)\lorG \phi

Wichtige Eigenschaften[Bearbeiten]

Es gibt zwei Eigenschaften die der linearen temporalen Logik zugeschrieben werden: Sicherheit (safety), sagt aus dass etwas Unerwünschtes nie auftritt (G\neg\phi) und Lebendigkeit (liveness), was aussagt dass etwas Erwünschtes immer wieder passiert (GF\psi oder G(\phi \rightarrowF\psi)). Generell: Sicherheit ist eine Eigenschaft für welche ein Gegenbeispiel ein endliches Präfix besitzt, selbst wenn der zu untersuchende Pfad unendlich ist. Für die Lebendigkeit wiederum kann jedes endliche Präfix eines Gegenbeispiels, welches die Formel erfüllt, zu einem unendlichen Pfad verlängert werden.

Äquivalenzumformungen[Bearbeiten]

Folgende Äquivalenzumformungen sind möglich:

X ( \phi \or \psi ) \equiv X \phi \or X \psi

X ( \phi \and \psi ) \equiv X \phi \and X \psi

X \neg \phi \equiv \neg X \phi

X ( \phi U \psi ) \equiv ( X \phi ) U ( X \psi )

F ( \phi \or \psi ) \equiv F \phi \or F \psi

\neg F \phi \equiv G \neg \phi

G ( \phi \and \psi ) \equiv G \phi \and G \psi

\neg G \phi \equiv F \neg \phi

( \phi \and \psi ) U \rho \equiv ( \phi U \rho ) \and ( \psi U \rho )

\rho U ( \phi \or \psi ) \equiv ( \rho U \phi ) \or ( \rho U \psi )

F \phi \equiv F F \phi

G \phi \equiv G G \phi

\phi U \psi \equiv \phi U ( \phi U \psi )

F \phi \equiv \phi \or X F \phi

G \phi \equiv \phi \and X G \phi

\phi U \psi \equiv \psi \or ( \phi \and X ( \phi U \psi ) )

\phi W \psi \equiv \psi \or ( \phi \and X ( \phi W \psi ) )

\phi R \psi \equiv ( \phi \and \psi ) \or ( \psi \and X ( \phi R \psi ) )

Beziehungen zu anderen Logiken[Bearbeiten]

Lineare temporale Logik (LTL) ist eine Teilmenge der Computation Tree Logic* (CTL*), besitzt eine gemeinsame Teilmenge mit CTL ist jedoch weder Ober- noch Untermenge von CTL.

LTL ist äquivalent zur Prädikatenlogik mit einstelligen Relationssymbolen (P_i)_{i\ge 1} und der kleiner-Relation \text{FO}[<,(P_i)_{i\ge 1}], wie auch stern-freien regulären Ausdrücken.

Automatentheoretisches LTL Model Checking[Bearbeiten]

Ein wichtiger Weg zur Modellprüfung besteht darin, die gewünschten Eigenschaften (wie oben beschrieben) mit LTL-Operatoren auszudrücken und dann zu überprüfen, ob das Modell diese Eigenschaften erfüllt.

Ferner ist es möglich, einen zum Modell "äquivalenten" Büchi-Automaten zu erstellen und einen, der zur Negation der zu prüfenden Eigenschaft äquivalent ist. Der Schnitt der beiden nicht-deterministischen Büchi-Automaten ist leer, wenn das Modell die Eigenschaften erfüllt.

Siehe auch[Bearbeiten]

Weblinks[Bearbeiten]

 Commons: Lineare temporale Logik – Sammlung von Bildern, Videos und Audiodateien