Linear temporal logic

Linear temporal logic

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, wie dass eine Bedingung irgendwann wahr wird, eine Bedingung wahr bleibt bis eine andere Bedingung erfüllt wird, usw.

Inhaltsverzeichnis

Syntax

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

  • X für Nachfolger (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 φ eine syntaktisch korrekte Formel ist, wenn φ syntaktisch korrekt ist. Die letzten zwei Operatoren sind binär, so dass φ U ψ eine syntaktisch korrekte Formel ist, wenn φ und ψ syntaktisch korrekte Formeln sind.

Semantik

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 φ \circ \phi nächster: φ gilt am nächsten Zustand. Bild:Ltlnext.png
G φ \Box \phi Global: φ gilt auf dem kompletten nachfolgenden Pfad. Bild:Ltlalways.png
F φ \Diamond \phi Finally: φ gilt irgendwann auf dem nachfolgenden Pfad. Bild:Ltlevently.png
Zweistellige Verknüpfungen:
ψ U φ \psi\mathcal{U}\phi Until: φ gilt an der aktuellen oder einer nachfolgenden Position und ψ gilt solange bis diese Position erreicht ist. An dieser Position muss ψ nicht mehr gelten. Bild:Ltluntil.png
ψ R φ \psi\mathcal{R}\phi Release: φ gilt bis zur ersten Position, an der ψ gilt oder für immer, wenn eine solche Position nicht existiert. Bild:Ltlrelease1.png

Bild:Ltlrelease2.png

Bereits zwei der Operatoren sind fundamental, d. h. sie definieren die anderen indem sie verknüpft werden:

  • F φ = true U φ
  • G φ = false R φ = \neg F \negφ
  • ψ R φ = \neg(\negψ U \negφ)

Sonderverknüpfungen

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:

  • ψ U φ = F φ\land(ψ W φ)
  • ψ R φ = φ W (ψ\landφ)
  • φ W ψ = ψ R (ψ\lorφ)
  • φ W ψ = (φ U ψ)\lorG φ

Wichtige Eigenschaften

Es gibt zwei Eigenschaften die der linearen temporalen Logik zugeschrieben werden: Sicherheit (safety), sagt aus dass etwas unerwünschtes nie auftritt (G\negφ) und Lebendigkeit (liveness), was aussagt dass etwas erwünschtes immer wieder passiert (GFψ oder G(\phi \rightarrowFψ)). 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 zu einem unendlichen Pfad verlängert werden, das die Formel erfüllt.

Äquivalenzumformungen

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

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

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 einem Nachfolger und der kleiner-Relation, FO[S,<] wie auch stern-freien regulären Ausdrücken oder deterministischen endlichen Automaten mit einer Schleifenkomplexität von 0.

Automata theoretic Linear temporal logic model checking

Ein wichtiger Weg zur Modellprüfung ist die gewünschten Eigenschaften (wie oben beschrieben) mit LTL-Operatoren zum Ausdruck zu bringen und tatsächlich überprüfen, ob das Modell diese Eigenschaft erfüllt.

Eine Möglichkeit ist es einen zum Modell "äquivalenten" Büchi-Automaten zu erstellen und einen, der zur Negation äquivalent ist. Der Schnitt der beiden nicht-deterministischen Büchi-Automaten ist leer, wenn das Modell die Eigenschaften erfüllt.

Siehe auch: Computation Tree Logic (CTL)

Weblinks


Wikimedia Foundation.

Игры ⚽ Поможем решить контрольную работу

Schlagen Sie auch in anderen Wörterbüchern nach:

  • Linear temporal logic — (LTL) is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths such as that a condition will eventually be true, that a condition will be true until another fact becomes true,… …   Wikipedia

  • Temporal logic — In logic, the term temporal logic is used to describe any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. It is sometimes also used to refer to tense logic, a particular modal logic… …   Wikipedia

  • Temporal logic in finite-state verification — In finite state verification, model checkers examine finite state machines representing concurrent software systems looking for errors in design. Errors are defined as violations of requirements expressed as properties of the system. In the event …   Wikipedia

  • Linear Time Temporal Logic — Die Computation Tree Logic (kurz CTL) ist eine Temporale Logik, die speziell zur Spezifikation und Verifikation von Computersystemen dient. Meist wird sie auch mit CTL* bezeichnet. CTL bezeichnet dann eine spezielle Teilmenge der CTL* Formeln.… …   Deutsch Wikipedia

  • Logic — For other uses, see Logic (disambiguation). Philosophy …   Wikipedia

  • Modal logic — is a type of formal logic that extends classical propositional and predicate logic to include operators expressing modality. Modals words that express modalities qualify a statement. For example, the statement John is happy might be qualified by… …   Wikipedia

  • Computation tree logic — Computation tree logic (CTL) is a branching time logic, meaning that its model of time is a tree like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is… …   Wikipedia

  • Lógica temporal — La lógica temporal es una extensión de la lógica modal, la cual es practicamente usada en sistema de reglas, donde esta presente el tiempo. Existe una cierta relación con otras variedades de lógica, por ejemplo, la lógica modal. Su estudio tiene… …   Wikipedia Español

  • Description logic — (DL) is a family of formal knowledge representation languages. It is more expressive than propositional logic but has more efficient decision problems than first order predicate logic. DL is used in artificial intelligence for formal reasoning on …   Wikipedia

  • Computational tree logic — Computation tree logic (CTL) is a branching time logic, meaning that its model of time is a tree like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”