Hennessy-Milner Logic in CSLib, the Lean Computer Science Library
Fabrizio Montesi, Marco Peressotti, Alexandre Rademaker
TL;DR
The paper formalises Hennessy-Milner Logic (HML) for labelled transition systems (LTS) within the Lean-based CSLib, providing a universe-polymorphic syntax, satisfaction, and denotational semantics, along with a complete metatheory. It proves the Hennessy-Milner theorem that, for image-finite LTSs, theory equivalence coincides with strong bisimilarity, and establishes the correctness of the denotational semantics and bisimulation invariance. The development is integrated with CSLib's LTS API and bisimilarity infrastructure, enabling direct application to CCS and automata defined in CSLib. All code is publicly available, verified with Lean 4.28.0-rc1, and designed for reuse across CSLib projects.
Abstract
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.