💻 computer science

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

Questo articolo presenta una formalizzazione a livello di libreria della Logica di Hennessy-Milner all'interno di CSLib, la libreria Lean per l'informatica, includendo sintassi, semantica e una metateoria completa che stabilisce l'equivalenza tra bisimulazione ed equivalenza teorica per sistemi di transizione etichettati a immagine finita.

Autori originali: Fabrizio Montesi, Marco Peressotti, Alexandre Rademaker

Pubblicato 2026-02-18

📖 4 min di lettura☕ Lettura da pausa caffè

CC BY 4.0

Autori originali: Fabrizio Montesi, Marco Peressotti, Alexandre Rademaker

Articolo originale sotto licenza CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Questa è una spiegazione generata dall'IA dell'articolo qui sotto. Non è stata scritta né approvata dagli autori. Per precisione tecnica, consulta l'articolo originale. Leggi il disclaimer completo

🏗️ Costruire un "Cervello" per le Macchine: La Logica di Hennessy-Milner in Lean

Immagina di avere un mondo pieno di macchine complesse (come robot, protocolli di comunicazione o software). Queste macchine fanno cose: si muovono, cambiano stato, inviano messaggi. In informatica, le chiamiamo Sistemi a Transizione Etichettata (LTS).

Il problema è: come facciamo a essere sicuri che due di queste macchine si comportino esattamente allo stesso modo? O meglio, come possiamo dire che due macchine sono "gemelle" nel loro comportamento?

Gli autori di questo articolo (Fabrizio, Marco e Alexandre) hanno creato un manuale di istruzioni universale (una "libreria") per rispondere a questa domanda, usando un linguaggio speciale chiamato Lean, che è come un assistente matematico super-potente che non sbaglia mai.

Ecco i concetti chiave, spiegati con delle metafore:

1. La Logica come un "Detective" (HML)

Hanno formalizzato una logica chiamata Hennessy-Milner Logic (HML).
Immagina l'HML come un detective che interroga una macchina. Il detective fa domande specifiche basate su ciò che la macchina può fare:

"Esiste almeno una strada che puoi prendere per arrivare a un posto dove c'è un tesoro?" (Questo è il modale "diamante" $\langle\mu\rangle$ ).
"Tutte le strade che puoi prendere ti portano a un posto sicuro?" (Questo è il modale "scatola" $[\mu]$ ).

Se una macchina risponde "Sì" a tutte le domande del detective, significa che soddisfa quella logica.

2. Il Grande Teorema: "Gemelli o Estranei?"

Il cuore del lavoro è un teorema famoso (il Teorema di Hennessy-Milner).
Immagina due macchine, la Macchina A e la Macchina B.

Se sono gemelle perfette (in gergo tecnico: bisimili), allora risponderanno esattamente allo stesso modo a tutte le domande del detective. Non c'è nessuna domanda che l'una sappia rispondere e l'altra no.
Il punto geniale: Il teorema dice che vale anche il contrario! Se due macchine rispondono allo stesso modo a tutte le domande possibili del detective, allora devono essere gemelle perfette. Non c'è differenza nascosta.

Attenzione: Questo funziona perfettamente solo se le macchine non hanno un numero infinito di strade da prendere in un singolo istante (in gergo: se sono "image-finite"). È come dire: "Se hai un numero infinito di opzioni, il detective potrebbe non riuscire a controllarle tutte in tempo".

3. La Libreria CSLib: Il "Lego" per gli Informatici

Finora, creare queste prove era come costruire un castello di Lego ogni volta da zero, pezzo per pezzo, rischiando di perdere un tassello.
Gli autori hanno creato una Libreria (CSLib) in Lean.

Cos'è? È una cassetta degli attrezzi già pronta.
Cosa contiene? La grammatica delle domande (sintassi), le regole per rispondere (semantica) e le prove matematiche che confermano che il detective funziona (metateoria).
Perché è speciale? È fatta in modo che chiunque usi i mattoncini Lego di questa libreria possa applicare le regole del detective a qualsiasi tipo di macchina, senza dover riscrivere le regole ogni volta. È come avere un manuale di istruzioni universale che funziona per le auto, per gli aerei e per i treni, purché usino lo stesso tipo di ruote.

4. L'Automazione: Il "Grind"

Una parte molto bella del lavoro è che hanno usato un'automazione chiamata tactic grind.
Immagina di dover dimostrare che un castello di Lego è stabile. Invece di controllare ogni singolo tassello a mano (che richiederebbe anni), hai un robot che scansiona tutto il castello in un secondo e ti dice: "Tutto a posto, è stabile!".
Gli autori hanno scritto il codice in modo che questo robot possa verificare automaticamente le loro prove matematiche. Questo rende il lavoro molto più veloce e sicuro.

In Sintesi: Perché è importante?

Questo articolo non è solo una teoria astratta. È un ponte tra la matematica pura e l'ingegneria del software reale.

Sicurezza: Permette di verificare con certezza matematica che due sistemi (ad esempio, due versioni diverse di un protocollo di sicurezza) si comportino allo stesso modo.
Riutilizzabilità: Una volta costruita questa "cassetta degli attrezzi" in Lean, chiunque studi automi, reti o processi concorrenti può usarla subito senza reinventare la ruota.
Futuro: È il primo passo per costruire sistemi informatici più sicuri, dove possiamo essere certi al 100% che il software fa esattamente quello che diciamo che deve fare.

In poche parole: hanno creato un linguaggio universale e un robot-verificatore per assicurarsi che le macchine digitali siano "gemelle" quando dovrebbero esserlo, e diverse quando dovrebbero esserlo, eliminando ogni dubbio.

Panoramica

Il paper presenta una formalizzazione a livello di libreria della Logica di Hennessy–Milner (HML) all'interno di CSLib (Computer Science Library), un progetto comunitario in rapida crescita basato sul theorem prover Lean 4. L'obiettivo è fornire una base logica rigorosa e riutilizzabile per i Sistemi a Transizione Etichettata (LTS), integrandosi profondamente con l'infrastruttura esistente di Lean e Mathlib.

1. Il Problema

I Sistemi a Transizione Etichettata (LTS) sono il framework standard per definire il comportamento operativo di molti sistemi computazionali (calcoli di processo, protocolli di comunicazione, automi). La Logica di Hennessy–Milner è fondamentale per ragionare su tali sistemi.
Tuttavia, nonostante il suo status fondazionale, le formalizzazioni meccanizzate di HML a "livello di libreria" con un'alta generalità sono scarse. Le implementazioni esistenti tendono a:

Trattare solo variazioni specifiche di HML.
Essere vincolate a tipi specifici di LTS.
Non integrarsi bene con ecosistemi di verifica più ampi.

Il paper mira a colmare questo vuoto fornendo una formalizzazione generale, parametrica e riutilizzabile che supporti la teoria completa, incluso il teorema di Hennessy–Milner.

2. Metodologia

Gli autori hanno sviluppato la formalizzazione utilizzando Lean 4 e la sua libreria matematica Mathlib. La metodologia si basa su tre pilastri principali:

Parametricità e Generalità: Le definizioni sono universe-polimorfe e parametriche rispetto a tipi arbitrari di stati e etichette di transizione. Questo permette di applicare la logica a qualsiasi LTS definito in CSLib senza modifiche.
Integrazione con l'Infrastruttura CSLib: La formalizzazione non è un'isola isolata, ma si integra direttamente con le definizioni esistenti di CSLib, in particolare per quanto riguarda la formalizzazione della bisimilarità e le API degli LTS.
Automazione delle Prove: Sfruttando le capacità di Lean, in particolare il tactic grind, gli autori hanno automatizzato gran parte delle dimostrazioni metateoriche, riducendo il carico manuale e garantendo robustezza.

3. Componenti della Formalizzazione

La formalizzazione copre l'intero ciclo di vita della logica:

Sintassi: Definizione induttiva delle proposizioni HML (true, false, and, or, diamond $\langle\mu\rangle$ , box $[\mu]$ ). Gli autori scelgono di includere false invece della negazione diretta nella sintassi base, definendo la negazione come una funzione derivata per mantenere la definizione della relazione di soddisfacimento elegante e ricorsiva.
Relazione di Soddisfacimento (Semantica Operativa): Definizione induttiva della relazione $s \models \phi$ (uno stato soddisfa una proposizione), basata sulle transizioni dell'LTS.
Semantica Denotazionale: Mappatura composizionale di ogni proposizione all'insieme degli stati che la soddisfano.
Equivalenza Teorica: Definizione della "teoria" di uno stato (l'insieme di tutte le proposizioni che soddisfa) e dell'equivalenza teorica tra stati.

4. Risultati Chiave e Metateoria

Il contributo principale risiede nella formalizzazione completa della metateoria di HML, che include:

Correttezza della Semantica Denotazionale (Teorema 1): Dimostrazione che la relazione di soddisfacimento induttiva coincide con la semantica denotazionale ( $s \models \phi \iff s \in \llbracket \phi \rrbracket$ ).
Invarianza della Bisimulazione (Teorema 2): Se due stati sono bisimili, non possono essere distinti logicamente da alcuna proposizione HML. Questo implica che la bisimilarità è un sottoinsieme dell'equivalenza teorica.
Teorema di Hennessy–Milner (Teorema 3): Il risultato fondamentale. Per gli LTS image-finite (dove l'insieme degli stati raggiungibili con una data etichetta è finito), l'equivalenza teorica implica la bisimilarità.
- Nota tecnica: La dimostrazione richiede un argomento creativo che sfrutta l'ipotesi di image-finitezza per costruire una proposizione distinguente che porta a una contraddizione se si assume che gli stati non siano bisimili.
Equivalenza Finale: Per gli LTS image-finite, la bisimilarità e l'equivalenza teorica coincidono ( $TheoryEq = \sim$ ).

5. Significato e Impatto

Riutilizzabilità e Applicabilità: Essendo parte di CSLib, questa formalizzazione è immediatamente applicabile a qualsiasi sistema che utilizzi l'API LTS della libreria, inclusi la teoria degli automi e il Calcolo dei Sistemi Comunicanti (CCS). Gli autori dimostrano questo applicando il teorema di Hennessy–Milner direttamente ai processi CCS definiti in CSLib.
Standard di Riferimento: Questo lavoro costituisce la prima formalizzazione di logica modale in CSLib e funge da implementazione di riferimento per future estensioni (ad esempio, verso equivalenze deboli o operatori di punto fisso).
Confronto con Lavori Precedenti: A differenza di formalizzazioni in altri prover (come Isabelle) che si concentrano su estensioni complesse (es. sistemi di transizione nominali per il $\pi$ -calcolo), questo approccio mantiene la fedeltà alla logica originale, risultando più semplice ma sufficientemente potente da provare la metateoria nella sua generalità.

In sintesi, il paper fornisce un'infrastruttura solida, automatizzata e generica per la verifica formale di sistemi concorrenti basati su HML, facilitando l'adozione di tecniche di model checking e verifica di proprietà in progetti di ricerca e sviluppo software verificato.