Hennessy-Milner Logic in CSLib, the Lean Computer Science Library

1. Problemstellung

Labelled Transition Systems (LTS) sind das Standard-Framework zur Definition des operationalen Verhaltens vieler computergestützter Systeme (z. B. Prozesskalküle, Kommunikationsprotokolle, Automaten). Hennessy–Milner Logic (HML) ist eine fundamentale modale Logik zur Spezifikation und Verifikation solcher Systeme. Ihr wichtigstes Merkmal ist der Hennessy–Milner-Satz, der besagt, dass für image-finite LTS (Systeme, bei denen jeder Zustand über eine Aktion nur endlich viele Nachfolger hat) zwei Zustände genau dann die gleichen HML-Formeln erfüllen, wenn sie stark bisimilar sind.

Trotz dieser fundamentalen Bedeutung gibt es einen Mangel an formalen, bibliotheksfähigen (library-grade) Mechanisierungen von HML in Theorembeweisern. Bestehende Arbeiten behandeln oft nur Variationen der Logik oder spezifische Arten von LTS. Es fehlte an einer allgemeinen, wiederverwendbaren Formalisierung innerhalb der Lean-Ökosystem-Infrastruktur, die nahtlos mit anderen Teilen der Computer Science Library (CSLib) integriert werden kann.

2. Methodik

Die Autoren haben eine vollständige Formalisierung von HML in Lean 4 als Teil des Lean Computer Science Library (CSLib) Projekts entwickelt. Der Ansatz zeichnet sich durch folgende methodische Merkmale aus:

• Parametrisierung: Die Definitionen sind universell-polymorph über beliebige Typen für Zustände und Transition-Labels. Sie sind nicht an spezifische Systemtypen gebunden, sondern nutzen die generische LTS-API von CSLib.
• Integration in Mathlib/CSLib: Die Entwicklung baut auf der etablierten Infrastruktur von Mathlib (der mathematischen Bibliothek für Lean) und CSLib auf, insbesondere auf der bereits vorhandenen Formalisierung von Bisimilarität.
• Automatisierung: Die Beweise nutzen stark die Automatisierungsfähigkeiten von Lean, insbesondere die grind-Taktik, um repetitive Beweisschritte (wie Induktionen über die Struktur von Formeln) automatisch abzuschließen.
• Design-Entscheidungen:
  • Die Syntax der Propositionen verzichtet auf ein direktes Negations-Operator-Symbol in der Grammatik, führt aber false ein. Die Negation wird als Funktion implementiert, die eine Formel in ihre negierte Form transformiert. Dies vereinfacht die Definition der Erfüllbarkeitsrelation (Satisfaction Relation) als elegante, rekursive Definition.
  • Es werden sowohl die induktive Erfüllbarkeitsrelation ($s \models \phi$) als auch eine denotationelle Semantik (Menge der erfüllenden Zustände) definiert.

3. Schlüsselbeiträge

Die Arbeit liefert drei Hauptbeiträge:

1. Formalisierung der Syntax und Semantik:

   • Definition der HML-Propositionen (True, False, Konjunktion, Disjunktion, Diamond $\langle\mu\rangle$, Box $[\mu]$) als induktiver Typ.
   • Definition der Erfüllbarkeitsrelation (Satisfies) als induktive Relation zwischen Zuständen und Formeln.
   • Definition der denotationellen Semantik, die jeder Formel die Menge der Zustände zuordnet, die sie erfüllen.
   • Definition von Theorie-Äquivalenz (Theory Equivalence): Zwei Zustände sind äquivalent, wenn sie dieselbe Menge an Formeln erfüllen.

2. Vollständige Metatheorie:

   • Korrektheit der Semantik: Beweis, dass die induktive Erfüllbarkeitsrelation und die denotationelle Semantik äquivalent sind ($s \models \phi \iff s \in \llbracket \phi \rrbracket$).
   • Bisimulations-Invarianz: Beweis, dass bisimulare Zustände logisch ununterscheidbar sind (wenn $s_1 \sim s_2$, dann erfüllen sie dieselben Formeln).
   • Hennessy–Milner-Theorem: Der zentrale Beweis, dass für image-finite LTS die Theorie-Äquivalenz genau der Bisimilarität entspricht ($TheoryEq \iff \sim$). Der Beweis nutzt die Endlichkeit der Bilder, um eine widersprüchliche Annahme (dass ein Zustand keine passende Transition hat) durch die Konstruktion einer unterscheidenden Formel zu widerlegen.

3. Integration und Wiederverwendbarkeit:

   • Die Bibliothek ist vollständig in CSLib integriert und bietet eine saubere API für nachgelagerte Anwendungen.
   • Die Autoren demonstrieren die Anwendbarkeit, indem sie zeigen, dass die Ergebnisse direkt auf in CSLib definierte Systeme wie Automatentheorie und den Calculus of Communicating Systems (CCS) angewendet werden können.

4. Ergebnisse

• Der Code ist öffentlich im CSLib-Repository verfügbar und wurde mit Lean 4.28.0-rc1 verifiziert.
• Die Beweise sind robust und nutzen Lean's Automatisierung effektiv; viele Fälle werden vollständig von der grind-Taktik gelöst.
• Es wurde gezeigt, dass die Theorie-Äquivalenz in CCS (unter der Bedingung der Bild-Endlichkeit, z. B. durch guardierte Rekursion) mit der Bisimilarität übereinstimmt.
• Die Arbeit stellt die erste modale Logik-Formalisierung in CSLib dar und dient als Referenzimplementierung für zukünftige Erweiterungen.

5. Bedeutung und Ausblick

Diese Arbeit schließt eine Lücke in der formalen Verifikation, indem sie HML nicht als isoliertes Beispiel, sondern als wiederverwendbare, allgemeine Bibliothekskomponente bereitstellt.

• Generalität: Durch die Parametrisierung über beliebige LTS-Typen ist die Bibliothek universell einsetzbar für alle Systeme, die die CSLib-LTS-Schnittstelle nutzen.
• Basis für Erweiterungen: Da die Metatheorie (insbesondere der Hennessy–Milner-Satz) bereits bewiesen ist, können zukünftige Arbeiten auf dieser Basis aufbauen, ohne die Grundlagen neu beweisen zu müssen.
• Zukünftige Arbeiten: Die Autoren identifizieren Erweiterungen als nächste Schritte, darunter:
  • Behandlung schwacher Äquivalenzen (Weak Bisimulation).
  • Einführung von Fixpunkt-Operatoren (für rekursive Spezifikationen).
  • Anpassung für Prozesskalküle mit gebundenen Variablen (wie $\pi$-Kalkül), was eine Erweiterung der Logik erfordert, um an Namen gebundene Transitionen zu handhaben (im Gegensatz zu den hier behandelten nominalen Transition Systems).

Zusammenfassend bietet das Paper eine solide, gut integrierte und formal verifizierte Grundlage für die logische Analyse von Transitionssystemen innerhalb des Lean-Ökosystems.