Mu-Calculus

LTL und CTL sind schön lesbar. Aber wie programmiert man den Checker? Der Wahre Kern der Verifikation ist Rekursion (Fixpunkte). "Immer X" heißt eigentlich: "Jetzt X, und danach wieder 'Immer X'". Der Mu-Calculus ist die "Maschinensprache" der Temporallogik. Er ist extrem kryptisch ($\mu Z . \phi \lor \Diamond Z$). Aber er ist mächtiger als LTL und CTL zusammen. Alles lässt sich in Mu-Calculus übersetzen. Er basiert auf dem Least Fixed Point ($\mu$) und Greatest Fixed Point ($\nu$).

Merksatz: Eine Erweiterung der Modallogik durch Fixpunkt-Operatoren, die eine extrem expressive (aber schwer lesbare) Sprache zur Beschreibung von rekursiven Eigenschaften in Prozessgraphen bietet.

Du als Mensch nutzt ihn fast nie (zu schwer zu lesen). Dein Tool (Model Checker) nutzt ihn intern. Du schreibst CTL. Der Compiler übersetzt es in Mu-Calculus. Die Engine löst den Fixpunkt.

1. Fixpunkte

$\mu$ (Least Fixed Point): Endliche Rekursion. "Irgendwann muss es passieren" (Liveness). Wie eine Schleife, die terminieren muss. ($EF \phi = \mu Z . \phi \lor \exists X Z$).
$\nu$ (Greatest Fixed Point): Unendliche Rekursion. "Es darf ewig so weitergehen" (Safety / Invariant). Wie eine Endlosschleife, die okay ist. ($AG \phi = \nu Z . \phi \land \forall X Z$).

2. Model Checking Games

Man kann Mu-Calculus als Spiel lösen. Angreifer (will beweisen, dass Formel falsch) vs. Verteidiger (will beweisen, wahr). Sie ziehen durch den Graphen. Wer nicht mehr ziehen kann (oder in einer ungünstigen Schleife landet), verliert. Das ist die modernste Art, Model Checking zu implementieren (Parity Games).

1. Alternation Depth

Die Komplexität des Mu-Calculus hängt massiv von der Alternation Depth ab. Das ist die Anzahl der Verschachtelungen von $\mu$ und $\nu$.

Tiefe 1: Einfach (LTL/CTL Niveau).
Tiefe 2+: "Mind-Blowing". Die Rechenzeit für das Model Checking wächst exponentiell mit der Tiefe. Mathematisch gesehen entspricht die Alternation Depth der Anzahl der notwendigen Prioritäten in einem Parity Game. Programme mit hoher Alternation Depth sind für Menschen quasi unmöglich zu debuggen – sie sind die "Assembler-Ebene" der formalen Logik.

2. Zusammenhang zu Parity Games

Die Lösung einer Mu-Calculus Formel auf einem endlichen Graphen ist äquivalent zum Lösen eines Parity Games. Das ist ein Spiel auf einem Graphen, bei dem jeder Knoten eine Priorität (Zahl) hat. Wenn die höchste unendlich oft besuchte Priorität gerade ist, gewinnt Spieler 0. Wenn sie ungerade ist, Spieler 1. Lange war unbekannt, ob man diese Spiele in Polynomialzeit lösen kann. 2017 wurde ein quasi-polynomieller Algorithmus gefunden. Das war eine Sensation in der theoretischen Informatik, da es bedeutet, dass wir selbst extrem komplexe rekursive Logiken viel schneller prüfen können, als wir dachten.

3. Expressivität nach Emerson & Clarke

E. Allen Emerson und Edmund M. Clarke (Turing-Preisträger) haben bewiesen: Der Mu-Calculus ist genau so mächtig wie die Monadic Second-Order Logic (MSO) auf Bäumen. Das bedeutet, dass jede Eigenschaft, die man über die Struktur eines Computerprogramms (als Baum/Graph) überhaupt formal sagen kann, im Mu-Calculus ausdrückbar ist. Er ist die ultimative Grenze dessen, was wir mit Logik verifizieren können.