Hennessy-Milner Logic in CSLib, the Lean Computer Science Library
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866917277845159936 |
|---|---|
| author | Montesi, Fabrizio Peressotti, Marco Rademaker, Alexandre |
| author_facet | Montesi, Fabrizio Peressotti, Marco Rademaker, Alexandre |
| contents | We present a library-level formalisation of Hennessy-Milner Logic (HML) - a foundational logic for labelled transition systems (LTSs) - for the Lean Computer Science Library (CSLib). Our development includes the syntax, satisfaction relation, and denotational semantics of HML, as well as a complete metatheory including the Hennessy-Milner theorem - bisimilarity coincides with theory equivalence for image-finite LTSs. Our development emphasises generality and reusability: it is parametric over arbitrary LTSs, definitions integrate with CSLib's infrastructure (such as the formalisation of bisimilarity), and proofs leverage Lean's automation (notably the grind tactic). All code is publicly available in CSLib and can be readily applied to systems that use its LTS API. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_15409 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Hennessy-Milner Logic in CSLib, the Lean Computer Science Library Montesi, Fabrizio Peressotti, Marco Rademaker, Alexandre Logic in Computer Science Programming Languages We present a library-level formalisation of Hennessy-Milner Logic (HML) - a foundational logic for labelled transition systems (LTSs) - for the Lean Computer Science Library (CSLib). Our development includes the syntax, satisfaction relation, and denotational semantics of HML, as well as a complete metatheory including the Hennessy-Milner theorem - bisimilarity coincides with theory equivalence for image-finite LTSs. Our development emphasises generality and reusability: it is parametric over arbitrary LTSs, definitions integrate with CSLib's infrastructure (such as the formalisation of bisimilarity), and proofs leverage Lean's automation (notably the grind tactic). All code is publicly available in CSLib and can be readily applied to systems that use its LTS API. |
| title | Hennessy-Milner Logic in CSLib, the Lean Computer Science Library |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2602.15409 |