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

A continuación presento un resumen técnico detallado del artículo "Hennessy–Milner Logic in CSLib, the Lean Computer Science Library", traducido y adaptado al español.

Resumen Técnico: Formalización de la Lógica Hennessy-Milner en CSLib

1. Problema y Contexto

Los Sistemas de Transición Etiquetada (LTS) son el marco estándar para definir el comportamiento operacional de sistemas computacionales como cálculos de procesos, protocolos de comunicación y autómatas. La Lógica Hennessy-Milner (HML) es una lógica modal fundamental para razonar sobre estos sistemas. Su característica distintiva es el Teorema de Hennessy-Milner, que establece que, en LTS con imágenes finitas, dos estados son indistinguibles lógicamente (satisfacen las mismas proposiciones) si y solo si son bisimilares.

A pesar de su importancia teórica, las formalizaciones mecanizadas de HML a nivel de biblioteca (con generalidad y reutilización) son escasas. Las existentes suelen tratar variaciones específicas de la lógica o tipos concretos de LTS, careciendo de una integración profunda con infraestructuras de verificación modernas que permitan su aplicación directa en diversos dominios.

2. Metodología

Los autores desarrollaron una formalización completa de HML utilizando el asistente de pruebas Lean 4, integrada dentro de CSLib (la Biblioteca de Ciencias Computacionales de Lean). La metodología se basó en los siguientes pilares:

• Parametrización Universal: Las definiciones son polimórficas en el universo, permitiendo que la lógica funcione sobre cualquier tipo de estados y etiquetas de transición, no solo casos específicos.
• Integración con CSLib y Mathlib: La formalización se construyó sobre la infraestructura existente de CSLib (para semántica operacional) y Mathlib (la biblioteca matemática de Lean), utilizando definiciones de conjuntos y tipos estándar.
• Automatización: Se aprovechó la táctica grind de Lean para automatizar gran parte de las pruebas, reduciendo la carga manual y garantizando la corrección de las definiciones recursivas.
• Enfoque en la Generalidad: A diferencia de trabajos previos que extendían HML para manejar variables ligadas (como en el cálculo $\pi$), este trabajo se adhiere a la definición original de HML para garantizar simplicidad y reutilización inmediata en sistemas basados en LTS estándar.

3. Contribuciones Clave

El artículo presenta tres contribuciones principales:

1. Definiciones Formales Completas:

   • Sintaxis: Un tipo inductivo para las proposiciones HML (true, false, and, or, diamond $\langle\mu\rangle$, box $[\mu]$). Se optó por incluir false en lugar de un operador de negación explícito para simplificar la definición de satisfacción, recuperando la negación mediante una función transformadora.
   • Relación de Satisfacción: Definida inductivamente (Satisfies), conectando los estados del LTS con las proposiciones lógicas.
   • Semántica Denotacional: Una función que mapea cada proposición al conjunto de estados que la satisfacen, demostrando la equivalencia con la relación de satisfacción inductiva.

2. Metateoría Completa de HML:

   • Corrección Semántica: Prueba de que la relación de satisfacción inductiva coincide exactamente con la semántica denotacional.
   • Invarianza de Bisimulación: Demostración de que si dos estados son bisimilares, satisfacen exactamente las mismas proposiciones.
   • Teorema de Hennessy-Milner: La prueba central que establece que, para LTS de imagen finita, la equivalencia de teorías (dos estados satisfacen las mismas proposiciones) es equivalente a la bisimulación. La prueba utiliza un argumento de contradicción basado en la finitud de las imágenes para construir una proposición distinguidora.

3. Integración y Aplicabilidad:

   • La biblioteca incluye APIs documentadas que permiten aplicar estos resultados directamente a otros componentes de CSLib, como la teoría de autómatas y el Cálculo de Sistemas de Comunicación (CCS).
   • Se demuestra que la equivalencia de teorías coincide con la bisimulación en implementaciones específicas de CCS dentro de la biblioteca.

4. Resultados

• Código Verificado: Todo el desarrollo fue verificado con Lean 4 (versión 4.28.0-rc1) y está disponible públicamente en el repositorio oficial de CSLib.
• Automatización Exitosa: El uso de la táctica grind permitió resolver automáticamente la mayoría de los casos de inducción en las pruebas de metateoría, validando la robustez de la infraestructura de Lean para este tipo de lógica.
• Generalidad Lograda: La formalización no está atada a un sistema específico; cualquier sistema que utilice la API de LTS de CSLib hereda automáticamente las propiedades de HML y el Teorema de Hennessy-Milner.

5. Significado e Impacto

Este trabajo representa la primera formalización de una lógica modal en CSLib, sirviendo como la implementación de referencia para HML. Su significado radica en:

• Cimentación de la Investigación: Proporciona una base confiable y reusable para futuras extensiones y aplicaciones dentro del ecosistema Lean, permitiendo verificar propiedades de sistemas concurrentes con rigor matemático.
• Puente entre Teoría y Práctica: Al integrar HML en una biblioteca de ciencias computacionales, facilita que investigadores y desarrolladores utilicen resultados teóricos profundos (como la equivalencia entre bisimulación y lógica) en el desarrollo de software verificado.
• Dirección Futura: Aunque el trabajo actual se centra en HML estándar, sienta las bases para futuras extensiones hacia equivalencias débiles, operadores de punto fijo y lógicas adaptadas a cálculos de procesos más complejos (como el cálculo $\pi$), abordando la necesidad de un marco general para extensiones de HML.

En resumen, el artículo no solo formaliza una lógica clásica, sino que demuestra cómo estructurarla dentro de una biblioteca moderna de ciencias computacionales para maximizar su utilidad, reutilización y corrección.