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

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

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

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

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

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

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

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

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.