imported>Valeee04: Die letzte Textänderung von Mr. Keks wurde verworfen und die Version 257175968 von SchlurcherBot wiederhergestellt. Grund: Das sieht nicht nach einer zu Bildungszwecke entwickelten Anwendung aus

2026-02-06T00:49:55Z

Die letzte Textänderung von Mr. Keks wurde verworfen und die Version 257175968 von SchlurcherBot wiederhergestellt. Grund: Das sieht nicht nach einer zu Bildungszwecke entwickelten Anwendung aus

Neue Seite

'''Lineare temporale Logik''' (''LTL'' oder ''Linear temporal logic'') ist eine formale [[Modallogik|modale]] [[temporale Logik]], die zur Modellprüfung aufgestellt und benutzt wird. In LTL können Formeln über die Zukunft von [[Weg (Graphentheorie)|Pfaden]] aufgestellt werden, beispielsweise dass eine Bedingung irgendwann wahr wird oder eine Bedingung wahr bleibt, bis eine andere Bedingung erfüllt wird.

== Syntax ==
LTL ist aus einer Menge von [[Aussagenvariable|Aussagenvariablen]] <math>p_1, p_2, ...</math>, den [[Logische Verknüpfung|logischen Verknüpfungen]] <math>\neg,\lor,\land,\rightarrow</math> und den nachfolgenden temporalen modalen Operatoren aufgebaut:
*'''X''' für Nachfolger (ne'''x'''t; '''N''' wird synonym benutzt)
*'''G''' für '''g'''lobal
*'''F''' für irgendwann ('''f'''inally)
*'''U''' für bis ('''u'''ntil)
*'''R''' für Auflösung ('''r'''elease).
Die ersten drei Operatoren sind [[Einstellige Verknüpfung|unär]], so dass '''X''' <math>\phi</math> eine [[syntaktisch]] korrekte Formel ist, wenn <math>\phi</math> syntaktisch korrekt ist. Die letzten zwei Operatoren sind binär, so dass <math>\phi</math> '''U''' <math>\psi</math> eine syntaktisch korrekte Formel ist, wenn <math>\phi</math> und <math>\psi</math> 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.

{| class="wikitable" align="center"
|-
!Textform
!Symbol
!Erklärung
!Beispielpfad
|-
| colspan="4" | [[Einstellige Verknüpfung]]en:
|-
|'''X''' <math>\phi</math>
|<math>\circ \phi</math>
|nächster (Ne'''X'''t): <math>\phi</math> gilt am nächsten Zustand.
|[[Datei:Ltlnext.png]]
|-
|'''G''' <math>\phi</math>
|<math>\Box \phi</math>
|'''G'''lobal: <math>\phi</math> gilt auf dem kompletten nachfolgenden Pfad.
|[[Datei:Ltlalways.png]]
|-
|'''F''' <math>\phi</math>
|<math>\Diamond \phi</math>
|'''F'''inally: <math>\phi</math> gilt irgendwann auf dem nachfolgenden Pfad.
|[[Datei:Ltlevently.png]]
|-
| colspan="4" | [[Zweistellige Verknüpfung]]en:
|-
|<math>\psi</math> '''U''' <math>\phi</math>
|<math>\psi\mathcal{U}\phi</math>
|'''U'''ntil: <math>\phi</math> gilt an der aktuellen oder einer nachfolgenden Position und <math>\psi</math> gilt mindestens solange, bis diese Position erreicht ist. An dieser Position muss <math>\psi</math> nicht mehr gelten.
|[[Datei:Ltluntil.png]]
|-
|<math>\psi</math> '''R''' <math>\phi</math>
|<math>\psi\mathcal{R}\phi</math>
|'''R'''elease: <math>\phi</math> gilt einschließlich bis zur ersten Position, an der <math>\psi</math> gilt, oder für immer, wenn eine solche Position nicht existiert.
|[[Datei:Ltlrelease1.png]]<br />
[[Datei:Ltlrelease2.png]]
|}

Bereits die zwei Operatoren '''X''' und '''U''' sind fundamental, das heißt, sie definieren die anderen durch geeignete Verknüpfungen:
*'''F''' <math>\phi</math> = '''true''' '''U''' <math>\phi</math>
*'''G''' <math>\phi</math> = '''false''' '''R''' <math>\phi</math> = <math>\neg</math> '''F''' <math>\neg</math><math>\phi</math>
*<math>\psi</math> '''R''' <math>\phi</math> = <math>\neg</math>(<math>\neg</math><math>\psi</math> '''U''' <math>\neg</math><math>\phi</math>)

== 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:
*<math>\psi</math> '''U''' <math>\phi</math> = '''F''' <math>\phi</math><math>\land</math>(<math>\psi</math> '''W''' <math>\phi</math>)
*<math>\psi</math> '''R''' <math>\phi</math> = <math>\phi</math> '''W''' (<math>\psi</math><math>\land</math><math>\phi</math>)
*<math>\phi</math> '''W''' <math>\psi</math> = <math>\psi</math> '''R''' (<math>\psi</math><math>\lor</math><math>\phi</math>)
*<math>\phi</math> '''W''' <math>\psi</math> = (<math>\phi</math> '''U''' <math>\psi</math>)<math>\lor</math>'''G''' <math>\phi</math>

== Wichtige Eigenschaften ==
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'''<math>\neg</math><math>\phi</math>) und Lebendigkeit (''liveness''), was aussagt, dass etwas Erwünschtes immer wieder passiert ('''GF'''<math>\psi</math> oder '''G'''<math>(\phi \rightarrow</math>'''F'''<math>\psi)</math>). 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 ==
Folgende [[Äquivalenzumformung]]en sind möglich:

<math>X ( \phi \lor \psi ) \equiv X \phi \lor X \psi</math>

<math>X ( \phi \land \psi ) \equiv X \phi \land X \psi</math>

<math>X \neg \phi \equiv \neg X \phi</math>

<math>X ( \phi U \psi ) \equiv ( X \phi ) U ( X \psi )</math>

<math>F ( \phi \lor \psi ) \equiv F \phi \lor F \psi</math>

<math>\neg F \phi \equiv G \neg \phi</math>

<math>G ( \phi \land \psi ) \equiv G \phi \land G \psi</math>

<math>\neg G \phi \equiv F \neg \phi</math>

<math>( \phi \land \psi ) U \rho \equiv ( \phi U \rho ) \land ( \psi U \rho )</math>

<math>\rho U ( \phi \lor \psi ) \equiv ( \rho U \phi ) \lor ( \rho U \psi )</math>

<math>F \phi \equiv F F \phi</math>

<math>G \phi \equiv G G \phi</math>

<math>\phi U \psi \equiv \phi U ( \phi U \psi )</math>

<math>F \phi \equiv \phi \lor X F \phi</math>

<math>G \phi \equiv \phi \land X G \phi</math>

<math>\phi U \psi \equiv \psi \lor ( \phi \land X ( \phi U \psi ) )</math>

<math>\phi W \psi \equiv \psi \lor ( \phi \land X ( \phi W \psi ) )</math>

<math>\phi R \psi \equiv ( \phi \land \psi ) \lor ( \psi \land X ( \phi R \psi ) )</math>

== Beziehungen zu anderen Logiken ==
Lineare temporale Logik (LTL) ist eine Teilmenge der [[Computation Tree Logic*]] (CTL*), besitzt eine gemeinsame Teilmenge mit [[Computation Tree Logic|CTL]] ist jedoch weder Ober- noch Untermenge von CTL.

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

== Automatentheoretisches LTL Model Checking ==
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-Automat]]en 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 ==
* [[Computation Tree Logic]] (CTL)

== Weblinks ==
{{Commonscat|Linear temporal logic|Lineare temporale Logik}}
* [https://www.mathematik.uni-marburg.de/~gumm/Lehre/SS07/ModelChecking/04_Lineare%20Temporale%20Logik.pdf P. Gumm - Lineare temporale Logik] von der Universität Marburg (PDF, 3,12 MB)
* [http://www.dcs.qmul.ac.uk/~pm/SaR/2004ltl.pdf A presentation of LTL] (englisch, PDF, 90 kB)
* [https://www.cmi.ac.in/~madhavan/papers/pdf/isical97.pdf Linear-Time Temporal Logic and Büchi Automata] (englisch, PDF, 212 kB)

[[Kategorie:Mathematische Logik]]
[[Kategorie:Temporale Logik]]

Lineare temporale Logik - Versionsgeschichte

imported>Valeee04: Die letzte Textänderung von Mr. Keks wurde verworfen und die Version 257175968 von SchlurcherBot wiederhergestellt. Grund: Das sieht nicht nach einer zu Bildungszwecke entwickelten Anwendung aus