💻 computer science

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

Dit artikel presenteert een herbruikbare formalisering van Hennessy-Milner-logica binnen de Lean Computer Science Library (CSLib), inclusief syntaxis, semantiek en een volledige metatheorie met het Hennessy-Milner-theorema voor beeld-finite LTS's.

Oorspronkelijke auteurs: Fabrizio Montesi, Marco Peressotti, Alexandre Rademaker

Gepubliceerd 2026-02-18

📖 4 min leestijd☕ Koffiepauze-leesvoer

CC BY 4.0

Oorspronkelijke auteurs: Fabrizio Montesi, Marco Peressotti, Alexandre Rademaker

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

De Digitale Spiegel: Hoe een Nieuw Boekje Computers helpt om elkaars gedrag te begrijpen

Stel je voor dat je een enorme verzameling robots hebt. Sommige robots zijn heel simpel, andere zijn ingewikkelde machines die constant communiceren met elkaar. Je wilt weten: Gedragen deze twee robots precies hetzelfde? Als robot A een knop indrukt en een lichtje laat branden, doet robot B dat dan ook? En als robot B stopt, stopt robot A dan ook?

In de wereld van informatica noemen we deze robots Labelled Transition Systems (LTS). Het zijn wiskundige modellen die beschrijven hoe systemen zich gedragen. Maar hoe bewijs je dat twee systemen echt identiek zijn? Soms lijken ze hetzelfde, maar hebben ze een klein, verborgen verschil.

Hier komt Hennessy-Milner Logic (HML) om de hoek kijken. Het is als een speciaal taalboekje of een detective-gids voor deze robots. Met dit boekje kun je vragen stellen over het gedrag van een robot, zoals: "Kan deze robot na een 'klik' een 'piep' maken?" of "Zal deze robot altijd stoppen als hij een 'stop'-signaal krijgt?"

Wat hebben deze onderzoekers gedaan?

Fabrizio Montesi, Marco Peressotti en Alexandre Rademaker hebben een heel belangrijk stuk werk gedaan voor CSLib. CSLib is een enorme, openbare bibliotheek voor de programmeertaal Lean. Je kunt Lean zien als een super-accurate rekenmachine die niet alleen getallen uitrekent, maar ook wiskundige bewijzen controleert.

De onderzoekers hebben een nieuwe, universele versie van dat HML-boekje in deze bibliotheek gebouwd. Hier is wat ze precies hebben gedaan, vertaald naar alledaags taal:

1. Het Bouwen van de Spelregels (Syntax en Semantiek)

Ze hebben de regels van het spel precies opgeschreven.

De vragen: Ze hebben gedefinieerd hoe je vragen kunt stellen (bijvoorbeeld: "Is er een weg naar een veilige toestand?" of "Is het altijd veilig?").
De antwoorden: Ze hebben een systeem bedacht om te controleren of een robot echt aan die vraag voldoet.
De betekenis: Ze hebben ook een manier bedacht om de "betekenis" van een vraag te vertalen naar een lijst met robots die het antwoord "ja" geven.

2. De Grootte van de Bibliotheek (Generality)

Het mooie aan hun werk is dat het niet alleen werkt voor één specifieke robot. Het werkt voor elke denkbare robot, zolang je maar de regels van de machine kent. Het is alsof ze een universele sleutel hebben gemaakt die op elke deur past, in plaats van een sleutel die alleen voor één deur werkt.

3. Het Gouden Bewijs: De Hennessy-Milner Stelling

Dit is het hoogtepunt van hun paper. Er is een beroemde theorie die zegt:

"Als twee robots precies dezelfde vragen in dit boekje kunnen beantwoorden, dan zijn ze ook echt identiek in hun gedrag."

Dit klinkt logisch, maar het is lastig om te bewijzen. De onderzoekers hebben dit bewezen voor een specifieke, maar zeer belangrijke groep robots: die waarbij je op elk moment een beperkt aantal volgende stappen kunt maken (de zogenaamde "image-finite" systemen).

De analogie:
Stel je voor dat je twee mensen hebt die je nog nooit hebt gezien. Je stelt ze een reeks vragen: "Kun je zwemmen?", "Kun je fietsen?", "Kun je dansen?".

Als ze op elke vraag exact hetzelfde antwoord geven, dan zijn ze (volgens deze theorie) in feite dezelfde persoon wat betreft hun vaardigheden.
De onderzoekers hebben in hun computerprogramma bewezen dat dit klopt, zolang de mensen maar een beperkt aantal vaardigheden hebben om te laten zien.

Waarom is dit zo cool?

Het werkt als een magische sleutel: Omdat dit werk is ingebouwd in de CSLib-bibliotheek, kunnen andere onderzoekers en ontwikkelaars dit direct gebruiken. Ze hoeven het niet zelf uit te vinden. Als ze een nieuw computersysteem bouwen (bijvoorbeeld voor verkeerslichten of beveiligingssoftware), kunnen ze dit boekje erbij pakken om te bewijzen dat hun systeem veilig en correct werkt.
Geen fouten mogelijk: Omdat het in Lean is geschreven, is elk bewijs door de computer gecontroleerd. Er is geen ruimte voor "misschien" of "ik denk wel". Het is 100% zeker.
De "Grind" Tactiek: De onderzoekers gebruiken een slimme truc in hun code genaamd grind. Dit is als een robot-assistent die automatisch alle kleine, saaie bewijstapjes doet, zodat de menselijke onderzoekers zich kunnen focussen op de grote, creatieve ideeën.

Samenvattend

Dit paper is als het bouwen van een fundering voor een nieuw huis. De onderzoekers hebben de betonnen vloer gelegd (de basisregels en het bewijs) waarop iedereen in de toekomst kan bouwen. Ze hebben laten zien dat je het gedrag van complexe computersystemen kunt beschrijven met een simpele taal, en dat je met wiskundige zekerheid kunt zeggen: "Ja, deze twee systemen zijn echt hetzelfde."

Dit helpt ontwikkelaars om software te maken die veiliger is, minder fouten bevat en beter werkt, of het nu gaat om een auto-pilot, een beveiligingssysteem of een netwerkprotocol.

Probleemstelling

Labelgedragen Transitiesystemen (LTS's) vormen de standaardkader voor het definiëren van het operationele gedrag van computationele systemen, zoals proceskalkulen, communicatieprotocollen en automata. Hennessy-Milner Logic (HML) is een fundamentele modale logica voor het redeneren over dergelijke systemen. De kern van HML wordt gevormd door de Hennessy-Milner stelling: voor image-finite LTS's (systemen waarbij elke toestand voor een gegeven label slechts eindig veel overgangen heeft) coinciden bisimilariteit en theorie-equivalentie.

Ondanks de fundamentele status van HML, ontbreekt er een bibliotheek-georiënteerde, generieke mechanisering in bewijshulpmiddelen. Bestaande formalisaties behandelen vaak specifieke variaties van HML of beperkte soorten LTS's, wat herbruikbaarheid en integratie met andere formele bibliotheken beperkt. Er was behoefte aan een universele, herbruikbare implementatie die naadloos integreert met bestaande infrastructuur voor computerwetenschap.

Methodologie

De auteurs hebben een volledige formalisatie van HML ontwikkeld in Lean 4, als onderdeel van de Lean Computer Science Library (CSLib). CSLib is een gemeenschapsproject dat een universele basis wil bieden voor formeel geverifieerd computerwetenschappelijk onderzoek.

De aanpak kenmerkt zich door:

Parametrisatie: De definities zijn universeel-polymorf en gelden voor willekeurige types van toestanden en labels, in plaats van vast te zitten aan een specifiek systeem.
Integratie met Mathlib en CSLib: De definities bouwen voort op de bestaande infrastructuur van CSLib (voor LTS's en bisimilariteit) en Mathlib (voor verzamelingen en eindigheid).
Automatisering: Bewijzen maken gebruik van Lean's geavanceerde automatisering, met name de grind tactic, die complexe gevallen automatisch kan oplossen door definities uit te vouwen en verzamelingoperaties te hanteren.
Designkeuzes: Voor de syntaxis van proposities is gekozen voor een variant zonder expliciete negatie-operator, maar wel met een false-propositie. Negatie wordt gedefinieerd als een transformatiefunctie. Dit maakt de definitie van de voldoendheidsrelatie (satisfaction relation) elegant en rechttoe rechtaan.

Kernbijdragen

Het artikel presenteert drie hoofdcomponenten:

Formalisatie van de Syntaxis en Semantiek:
- Syntaxis: Een inductieve definitie van HML-proposities (true, false, and, or, diamond $\langle\mu\rangle$ , box $[\mu]$ ).
- Voldoendheidsrelatie ( $s \models \varphi$ ): Een inductieve definitie die beschrijft wanneer een toestand een propositie voldoet, gebaseerd op de transitierelatie van het LTS.
- Denotationele Semantiek: Een compositional mapping die elke propositie afbeeldt op de verzameling van toestanden die deze voldoen.
- Theorie-equivalentie: Twee toestanden zijn theorie-equivalent als ze exact dezelfde verzameling proposities voldoen.
Volledige Metatheorie:
- Correctheid van de Semantiek: Bewezen dat de inductieve voldoendheidsrelatie en de denotationele semantiek equivalent zijn (een toestand voldoet aan $\varphi$ dan en slechts dan als deze tot de denotationele verzameling van $\varphi$ behoort).
- Bisimulatie-invariantie: Bewezen dat bisimulaire toestanden niet logisch te onderscheiden zijn (als $s_1 \sim s_2$ , dan geldt $s_1 \models \varphi \iff s_2 \models \varphi$ ).
- De Hennessy-Milner Stelling: Bewezen dat voor image-finite LTS's theorie-equivalentie impliceert dat toestanden bisimulair zijn. Het bewijs maakt gebruik van een constructieve aanpak waarbij, gezien de eindigheid van de afbeelding, een onderscheidende propositie kan worden geconstrueerd die een mismatch in gedrag blootlegt.
Integratie en Toepasbaarheid:
- De code is volledig geïntegreerd in CSLib met duidelijke API's en documentatie.
- De resultaten zijn direct toepasbaar op andere delen van CSLib, zoals de formalisatie van Automata-theorie en de Calculus of Communicating Systems (CCS).

Resultaten

De auteurs hebben een robuust, universeel formalisme voor HML gecreëerd dat volledig is geverifieerd in Lean 4 (versie 4.28.0-rc1).
De Hennessy-Milner stelling is succesvol bewezen voor het algemene geval van image-finite LTS's binnen dit framework.
De implementatie demonstreert dat complexe metatheoretische resultaten (zoals het bewijs dat theorie-equivalentie een bisimulatie is) efficiënt kunnen worden bewezen met Lean's automatisering (grind), hoewel het bewijs voor de Hennessy-Milner stelling enige creativiteit vereiste bij het construeren van de onderscheidende propositie.
Een voorbeeld toont aan dat de stelling direct geldt voor CCS-processen, zolang deze voldoen aan de image-finite voorwaarde (bijvoorbeeld via guarded recursion).

Significantie

Dit werk is significant omdat het de eerste modale logica-formalisatie is in CSLib en fungeert als de referentie-implementatie voor Hennessy-Milner Logic binnen deze bibliotheek.

Herbruikbaarheid: Door parametrisch te werken, kunnen ontwikkelaars van andere projecten die CSLib gebruiken (zoals verificatie van protocollen of automata) direct profiteren van de bewezen eigenschappen zonder de logica opnieuw te hoeven formaliseren.
Fundamentele Basis: Het biedt een solide basis voor toekomstige uitbreidingen, zoals zwakkere equivalenties, fixpoint-operatoren (voor mu-calculus) of uitbreidingen naar processen met gebonden variabelen (zoals in de $\pi$ -calculus).
Community Impact: Het project versterkt de positie van Lean als een platform voor geavanceerd computerwetenschappelijk onderzoek en demonstreert hoe fundamentele theorieën kunnen worden gebundeld in een herbruikbare, gemeenschappelijke bibliotheek.

Kortom, het artikel levert een essentiële, hoogwaardige bouwsteen voor formeel geverifieerde computerwetenschap, waarbij de brug wordt geslagen tussen abstracte theoretische logica en praktische, herbruikbare softwarebibliotheken.