www.wikidata.de-de.nina.az

Lineare temporale Logik LTL oder Linear temporal logic ist eine formale modale temporale Logik die zur Modellprüfung auf

Lineare temporale Logik

Lineare temporale Logik (LTL oder Linear temporal logic) ist eine formale modale temporale Logik, die zur Modellprüfung aufgestellt und benutzt wird. 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 , den logischen Verknüpfungen 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 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 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 nächster (NeXt): gilt am nächsten Zustand.
G Global: gilt auf dem kompletten nachfolgenden Pfad.
F Finally: gilt irgendwann auf dem nachfolgenden Pfad.
Zweistellige Verknüpfungen:
U Until: gilt an der aktuellen oder einer nachfolgenden Position und gilt mindestens solange, bis diese Position erreicht ist. An dieser Position muss nicht mehr gelten.
R Release: gilt einschließlich bis zur ersten Position, an der gilt, oder für immer, wenn eine solche Position nicht existiert.

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

  • F = true U
  • G = false R = F
  • R = ( U )

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:

  • U = F ( W )
  • R = W ()
  • W = R ()
  • W = ( U )G

Wichtige Eigenschaften Bearbeiten

Es gibt zwei wichtige Klassen von Eigenschaften, die mittels linearer temporaler Logik beschrieben werden können: Sicherheit (safety), sagt aus, dass etwas Unerwünschtes nie auftritt (G) und Lebendigkeit (liveness), was aussagt, dass etwas Erwünschtes immer wieder passiert (GF oder GF). Generell: Sicherheitseigenschaften sind solche, für die als Gegenbeispiel ein endliches Präfix ausreicht, dessen beliebige unendliche Verlängerung die Eigenschaft stets verletzt. Bei Lebendigkeitseigenschaften wiederum kann jeder beliebige endliche Präfix eines Pfads noch zu einem unendlichen Pfad verlängert werden, welcher die Formel erfüllt.

Äquivalenzumformungen Bearbeiten

Folgende Äquivalenzumformungen sind möglich:

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 und der kleiner-Relation , 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
wikipedia, wiki, deutsches, deutschland, buch, bücher, bibliothek artikel lesen, herunterladen kostenlos kostenloser herunterladen, MP3, Video, MP4, 3GP, JPG, JPEG, GIF, PNG, Bild, Musik, Lied, Film, Buch, Spiel, Spiele
Veröffentlichungsdatum:
Lineare temporale Logik LTL oder Linear temporal logic ist eine formale modale temporale Logik die zur Modellprufung aufgestellt und benutzt wird In LTL konnen Formeln uber die Zukunft von Pfaden aufgestellt werden beispielsweise dass eine Bedingung irgendwann wahr wird oder eine Bedingung wahr bleibt bis eine andere Bedingung erfullt wird Inhaltsverzeichnis 1 Syntax 2 Semantik 3 Sonderverknupfungen 4 Wichtige Eigenschaften 5 Aquivalenzumformungen 6 Beziehungen zu anderen Logiken 7 Automatentheoretisches LTL Model Checking 8 Siehe auch 9 WeblinksSyntax BearbeitenLTL ist aus einer Menge von Aussagenvariablen p 1 p 2 displaystyle p 1 p 2 nbsp den logischen Verknupfungen displaystyle neg lor land rightarrow nbsp und den nachfolgenden temporalen modalen Operatoren aufgebaut X fur Nachfolger next N wird synonym benutzt G fur global F fur irgendwann finally U fur bis until R fur Auflosung release Die ersten drei Operatoren sind unar so dass X ϕ displaystyle phi nbsp eine syntaktisch korrekte Formel ist wenn ϕ displaystyle phi nbsp syntaktisch korrekt ist Die letzten zwei Operatoren sind binar so dass ϕ displaystyle phi nbsp U ps displaystyle psi nbsp eine syntaktisch korrekte Formel ist wenn ϕ displaystyle phi nbsp und ps displaystyle psi nbsp syntaktisch korrekte Formeln sind Semantik BearbeitenEine LTL Formel kann sowohl uber einer unendlichen Sequenz von Aussagen als auch einer einzigen Position auf dem Pfad ausgewertet werden Eine LTL Formel ist genau dann auf einem Pfad erfullt wenn sie auf Position 0 des Pfades erfullt ist Die Semantik der modalen Operatoren ist wie folgt Textform Symbol Erklarung BeispielpfadEinstellige Verknupfungen X ϕ displaystyle phi nbsp ϕ displaystyle circ phi nbsp nachster NeXt ϕ displaystyle phi nbsp gilt am nachsten Zustand nbsp G ϕ displaystyle phi nbsp ϕ displaystyle Box phi nbsp Global ϕ displaystyle phi nbsp gilt auf dem kompletten nachfolgenden Pfad nbsp F ϕ displaystyle phi nbsp ϕ displaystyle Diamond phi nbsp Finally ϕ displaystyle phi nbsp gilt irgendwann auf dem nachfolgenden Pfad nbsp Zweistellige Verknupfungen ps displaystyle psi nbsp U ϕ displaystyle phi nbsp ps U ϕ displaystyle psi mathcal U phi nbsp Until ϕ displaystyle phi nbsp gilt an der aktuellen oder einer nachfolgenden Position und ps displaystyle psi nbsp gilt mindestens solange bis diese Position erreicht ist An dieser Position muss ps displaystyle psi nbsp nicht mehr gelten nbsp ps displaystyle psi nbsp R ϕ displaystyle phi nbsp ps R ϕ displaystyle psi mathcal R phi nbsp Release ϕ displaystyle phi nbsp gilt einschliesslich bis zur ersten Position an der ps displaystyle psi nbsp gilt oder fur immer wenn eine solche Position nicht existiert nbsp nbsp Bereits die zwei Operatoren X und U sind fundamental das heisst sie definieren die anderen durch geeignete Verknupfungen F ϕ displaystyle phi nbsp true U ϕ displaystyle phi nbsp G ϕ displaystyle phi nbsp false R ϕ displaystyle phi nbsp displaystyle neg nbsp F displaystyle neg nbsp ϕ displaystyle phi nbsp ps displaystyle psi nbsp R ϕ displaystyle phi nbsp displaystyle neg nbsp displaystyle neg nbsp ps displaystyle psi nbsp U displaystyle neg nbsp ϕ displaystyle phi nbsp Sonderverknupfungen BearbeitenEinige Autoren definieren einen schwachen bis Operator weak until mit W bezeichnet der eine ahnliche 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 konnen ps displaystyle psi nbsp U ϕ displaystyle phi nbsp F ϕ displaystyle phi nbsp displaystyle land nbsp ps displaystyle psi nbsp W ϕ displaystyle phi nbsp ps displaystyle psi nbsp R ϕ displaystyle phi nbsp ϕ displaystyle phi nbsp W ps displaystyle psi nbsp displaystyle land nbsp ϕ displaystyle phi nbsp ϕ displaystyle phi nbsp W ps displaystyle psi nbsp ps displaystyle psi nbsp R ps displaystyle psi nbsp displaystyle lor nbsp ϕ displaystyle phi nbsp ϕ displaystyle phi nbsp W ps displaystyle psi nbsp ϕ displaystyle phi nbsp U ps displaystyle psi nbsp displaystyle lor nbsp G ϕ displaystyle phi nbsp Wichtige Eigenschaften BearbeitenEs gibt zwei wichtige Klassen von Eigenschaften die mittels linearer temporaler Logik beschrieben werden konnen Sicherheit safety sagt aus dass etwas Unerwunschtes nie auftritt G displaystyle neg nbsp ϕ displaystyle phi nbsp und Lebendigkeit liveness was aussagt dass etwas Erwunschtes immer wieder passiert GFps displaystyle psi nbsp oder G ϕ displaystyle phi rightarrow nbsp Fps displaystyle psi nbsp Generell Sicherheitseigenschaften sind solche fur die als Gegenbeispiel ein endliches Prafix ausreicht dessen beliebige unendliche Verlangerung die Eigenschaft stets verletzt Bei Lebendigkeitseigenschaften wiederum kann jeder beliebige endliche Prafix eines Pfads noch zu einem unendlichen Pfad verlangert werden welcher die Formel erfullt Aquivalenzumformungen BearbeitenFolgende Aquivalenzumformungen sind moglich X ϕ ps X ϕ X ps displaystyle X phi lor psi equiv X phi lor X psi nbsp X ϕ ps X ϕ X ps displaystyle X phi land psi equiv X phi land X psi nbsp X ϕ X ϕ displaystyle X neg phi equiv neg X phi nbsp X ϕ U ps X ϕ U X ps displaystyle X phi U psi equiv X phi U X psi nbsp F ϕ ps F ϕ F ps displaystyle F phi lor psi equiv F phi lor F psi nbsp F ϕ G ϕ displaystyle neg F phi equiv G neg phi nbsp G ϕ ps G ϕ G ps displaystyle G phi land psi equiv G phi land G psi nbsp G ϕ F ϕ displaystyle neg G phi equiv F neg phi nbsp ϕ ps U r ϕ U r ps U r displaystyle phi land psi U rho equiv phi U rho land psi U rho nbsp r U ϕ ps r U ϕ r U ps displaystyle rho U phi lor psi equiv rho U phi lor rho U psi nbsp F ϕ F F ϕ displaystyle F phi equiv FF phi nbsp G ϕ G G ϕ displaystyle G phi equiv GG phi nbsp ϕ U ps ϕ U ϕ U ps displaystyle phi U psi equiv phi U phi U psi nbsp F ϕ ϕ X F ϕ displaystyle F phi equiv phi lor XF phi nbsp G ϕ ϕ X G ϕ displaystyle G phi equiv phi land XG phi nbsp ϕ U ps ps ϕ X ϕ U ps displaystyle phi U psi equiv psi lor phi land X phi U psi nbsp ϕ W ps ps ϕ X ϕ W ps displaystyle phi W psi equiv psi lor phi land X phi W psi nbsp ϕ R ps ϕ ps ps X ϕ R ps displaystyle phi R psi equiv phi land psi lor psi land X phi R psi nbsp Beziehungen zu anderen Logiken BearbeitenLineare 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 aquivalent zur Pradikatenlogik mit einstelligen Relationssymbolen P i i 1 displaystyle P i i geq 1 nbsp und der kleiner Relation FO lt P i i 1 displaystyle text FO lt P i i geq 1 nbsp wie auch stern freien regularen Ausdrucken Automatentheoretisches LTL Model Checking BearbeitenEin wichtiger Weg zur Modellprufung besteht darin die gewunschten Eigenschaften wie oben beschrieben mit LTL Operatoren auszudrucken und dann zu uberprufen ob das Modell diese Eigenschaften erfullt Ferner ist es moglich einen zum Modell aquivalenten Buchi Automaten zu erstellen und einen der zur Negation der zu prufenden Eigenschaft aquivalent ist Der Schnitt der beiden nicht deterministischen Buchi Automaten ist leer wenn das Modell die Eigenschaften erfullt Siehe auch BearbeitenComputation Tree Logic CTL Weblinks Bearbeiten nbsp Commons Lineare temporale Logik Sammlung von Bildern Videos und Audiodateien P Gumm Lineare temporale Logik von der Universitat Marburg PDF 3 12 MB A presentation of LTL englisch PDF 90 kB Linear Time Temporal Logic and Buchi Automata englisch PDF 212 kB Abgerufen von https de wikipedia org w index php title Lineare temporale Logik amp oldid 233615683