Linear Temporal Logic (LTL)

Operatoren (Buchstaben):

• X (Next): Im nächsten Schritt ist $\phi$ wahr. (X happy).
• G (Globally): Immer (ab jetzt) ist $\phi$ wahr. (G safe).
• F (Future): Irgendwann ist $\phi$ wahr. (F rich).
• U (Until): $\phi$ ist wahr, bis $\psi$ wahr wird. (hungry U eat). Beispiel Ampel: G (Red -> X Green). "Immer wenn Rot, ist im nächsten Schritt Grün." (Falsch! Meist kommt erst Gelb).

1. Model Checking (SPIN)

Der Model Checker SPIN nutzt LTL. Er nimmt dein C-Programm (oder Modell in Promela). Er nimmt deine LTL-Formel. Er bricht die Formel in einen "Büchi-Automaten" (sucht nach Gegenbeispielen). Er lässt das Programm Milliarden male laufen (simuliert). Findet er einen Pfad, der die Formel verletzt? -> Alarm.

2. Mächtigkeit

LTL kann Dinge ausdrücken wie "Fairness". G (F Request -> F Grant). "Immer gilt: Wenn ich anfrage, kriege ich irgendwann Zugriff." (Kein Starvation). Das kann man in einfacher Logik nicht sagen.

1. Omega-Regular Languages & Büchi Automata

Mathematisch beschreibt eine LTL-Formel nicht nur einen Satz, sondern eine Sprache. Eine Sprache über unendlichen Wörtern ($\omega$-Wörter). Um zu prüfen, ob ein Programm eine LTL-Formel erfüllt, übersetzt der Computer die Formel in einen Büchi-Automaten. Ein Büchi-Automat ist wie ein normaler Automat, aber er akzeptiert einen Pfad nur dann, wenn er einen Endzustand unendlich oft besucht. Der Model Checker berechnet dann das Kreuzprodukt aus deinem Programmautomaten und dem negierten Formel-Automaten. Wenn er einen Zyklus findet, der durch einen akzeptierenden Zustand geht, hat er ein Gegenbeispiel (ein "unendliches Fehlverhalten") gefunden.

2. Automata-Theoretic Model Checking

Warum ist LTL so beliebt in der Forschung? Wegen der algorithmischen Sauberkeit. Der Prozess folgt immer dem gleichen Schema:

1. Übersetze $\neg \Phi$ (die Eigenschaft, die NICHT passieren darf) in einen Büchi-Automaten $B_{\neg \Phi}$.
2. Stelle das System als Kripke-Struktur $M$ dar.
3. Prüfe, ob der Schnitt $M \cap B_{\neg \Phi}$ leer ist. Dieser Ansatz erlaubt es, hocheffiziente Algorithmen zur Suche im Zustandsraum zu nutzen (z.B. Nested Depth First Search), die nur Bits im Speicher umdrehen, ohne die komplexe Logik der Formel während der Suche "verstehen" zu müssen.

3. Fairness-Constraints in der Produktion

In echten verteilten Systemen (Cloud) ist LTL ohne Fairness nutzlos. Stell dir vor, du hast zwei Prozesse. Prozess A rechnet ewig. Prozess B wartet. Technisch ist "A rechnet ewig" ein gültiger Pfad. Aber in der Realität wird der Scheduler irgendwann zu B wechseln. Man nutzt daher Weak Fairness (FG halt -> F run) oder Strong Fairness (GF request -> GF grant). In der Expert-Ebene der Verifikation (z.B. mit TLA+ oder SPIN) muss man diese Fairness-Axiome explizit hinzufügen, damit der Model Checker nicht Milliarden von "unrealistischen" Gegenbeispielen ausspuckt, in denen ein Prozess einfach nur Glück hat und nie unterbrochen wird.