##  [Lineare Temporallogik (LTL)](/de/node/61333) 

 Definition

Eine Temporallogik, die über lineare Zeitstrukturen interpretiert wird, in denen Formeln über einzelne unendliche Sequenzen (Zeitlinien) ausgewertet werden; gängige Operatoren sind X (next), F (eventually), G (always) und U (until).

 

 

 

 

 

 





## Prinzip

Prinzip

Interpretation temporaler Modalitäten über einzelne Ausführungsspuren, so dass eine Formel mit Bezug auf eine einzelne lineare Zeitlinie wahr oder falsch ist; Quantifizierung über alternative Zukünfte fehlt, der Fokus liegt auf Eigenschaften von Sequenzen statt auf Verzweigungsbäumen von Möglichkeiten.

 

 

 

 

 





## Demonstration

Demonstration

In der Hardware-Verifikation sichert die LTL-Eigenschaft G(reset -> X ready), dass auf jeder taktgesteuerten Spur nach einem Reset im nächsten Zustand ready gilt; Model-Checker durchsuchen Spuren oder übersetzen LTL in Automaten, um solche Eigenschaften gegen eine Implementierung zu prüfen.

 

 

 

 

## Fehlanwendung

Fehlanwendung

LTL zur Spezifikation verzweigter Anforderungen zu verwenden, etwa anzunehmen, es gebe einen Zukunftspfad, auf dem φ immer gilt, obwohl Pfadquantifizierung nötig ist — solche Anforderungen lassen sich oft nur in verzweigter Logik wie CTL/CTL* ausdrücken.

 

 

 

 

 





## Konsequenz

Konsequenz

Richtige Anwendung von LTL liefert präzise, spurbezogene Spezifikationen von Sicherheits- (Invarianten) und Lebendigkeitseigenschaften (Eventualitäten) und erlaubt Reduktionen auf Automaten für die algorithmische Verifikation sequentieller Verhaltensweisen.

 

 

 

 

## Umkehrung

Umkehrung

Der Umkehrfall ist verzweigte Temporallogik, in der Formeln über mehrere mögliche Zukünfte ab einem Zustand quantifizieren; Eigenschaften, die explizite Pfadquantoren erfordern, lassen sich nicht in reinem LTL ausdrücken.

 

 

 

 

 





## Abgrenzung

Abgrenzung

LTL setzt lineare (oft unendliche) diskrete Zeit voraus und enthält ohne Erweiterung keine Pfadquantoren oder echtzeitliche Einschränkungen; sie ist nicht geeignet, wenn Eigenschaften inhärent über verschiedene mögliche Zukünfte eines Zustands quantifizieren.

 

 

 

 

 





## Semantische Spannung

Semantische Spannung

Es besteht Spannung zwischen LTL und verzweigten Logiken (CTL, CTL*): manche Eigenschaften sind in der einen einfach ausdrückbar, in der anderen nicht, und die Wahl bestimmt die geeigneten Model-Checking-Algorithmen und Automatenkonstruktionen.

 

 

 

 

 





## Synthese

Synthese

LTL ist der Teilbereich temporalen Denkens für Einspur-Spezifikationen: Durch Interpretation temporaler Operatoren entlang linearer Zeitlinien bietet sie eine kompakte, automatenfreundliche Sprache, um sequentielle temporale Eigenschaften von Systemen auszudrücken und zu prüfen.