Hennessy-Milner逻辑在CSLib中的实现
Hennessy-Milner Logic in CSLib, the Lean Computer Science Library
AI总结：
本文在Lean库中实现了Hennessy-Milner逻辑，提供了形式化定义、元理论及自动化证明方法，适用于标记转换系统的分析与验证。
摘要：
我们为Lean计算机科学库（CSLib）实现了Hennessy-Milner逻辑（HML）的库级形式化，这是一种用于标记转换系统（LTSs）的基础逻辑。我们的开发包括HML的语法、满足关系和指称语义，以及完整的元理论，包括Hennessy-Milner定理——对于图像有限的LTSs，双射等价性与理论等价性一致。我们的开发强调通用性和可重用性：它对任意LTSs参数化，定义与CSLib的基础设施（如双射形式化）集成，并利用Lean的自动化（特别是grind战术）。所有代码都公开在CSLib中，并可直接应用于使用其LTS API的系统。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
