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

Resumo Técnico: Formalização da Lógica de Hennessy–Milner no CSLib

1. Problema e Contexto

Os Sistemas de Transição Rotulada (LTS) são o framework padrão para definir o comportamento operacional de sistemas computacionais, como cálculos de processos, protocolos de comunicação e autômatos. A Lógica de Hennessy–Milner (HML) é uma lógica modal fundamental para raciocinar sobre esses sistemas. Sua característica distintiva é o Teorema de Hennessy–Milner, que estabelece que, em LTSs com imagens finitas, dois estados satisfazem exatamente as mesmas proposições HML se e somente se forem bisimilares (fortemente).

Apesar da importância fundacional da HML, o artigo identifica uma lacuna na literatura: há uma escassez de formalizações mecanizadas de HML com generalidade de nível de biblioteca. As formalizações existentes tendem a tratar variações específicas da lógica ou tipos particulares de LTS, em vez de oferecer uma base genérica e reutilizável.

2. Metodologia

Os autores desenvolveram uma formalização completa da HML utilizando o assistente de prova Lean 4, integrada ao CSLib (Lean Computer Science Library), um projeto comunitário em crescimento para fornecer uma base universal para pesquisa em ciência da computação formalizada.

A abordagem metodológica foca em:

• Generalidade e Reutilização: A definição é paramétrica sobre tipos arbitrários de estados e rótulos de transição, integrando-se à infraestrutura do CSLib (especificamente a API de LTS e a formalização de bisimulação).
• Abordagem Sintática: A linguagem de proposições HML foi definida como um tipo indutivo paramétrico, incluindo conectivos booleanos (true, false, and, or) e modais (diamond $\langle\mu\rangle$, box $[\mu]$). Optou-se por incluir false em vez de um conectivo de negação explícito na sintaxe base, permitindo uma definição elegante de negação como uma função derivada.
• Semântica Dupla:
  1. Relação de Satisfação ($s \models \varphi$): Definida indutivamente, relacionando estados a proposições com base nas transições do LTS.
  2. Semântica Denotacional: Mapeia cada proposição para o conjunto de estados que a satisfazem, utilizando operações de conjuntos (união, interseção, etc.).
• Automação: Os autores exploraram a automação do Lean, notavelmente a tática grind, para provar automaticamente a maioria dos casos indutivos, reduzindo a carga manual de prova.

3. Principais Contribuições

O artigo apresenta três contribuições principais:

1. Definições Polimórficas de Universos: Sintaxe, relação de satisfação e semântica denotacional da HML definidas de forma polimórfica, permitindo aplicação em qualquer tipo de LTS.
2. Metateoria Completa: Formalização e prova de todos os resultados metateóricos fundamentais da HML, incluindo:
   • A correção da semântica denotacional (equivalência entre satisfação indutiva e pertinência ao conjunto denotacional).
   • A invariância da bisimulação (estados bisimilares satisfazem as mesmas proposições).
   • O Teorema de Hennessy–Milner: A prova de que a equivalência teórica (satisfazer as mesmas proposições) coincide com a bisimilaridade para LTSs de imagem finita.
3. Integração e API: A implementação foi integrada ao CSLib com documentação e APIs adequadas, permitindo que projetos downstream (como a teoria de autômatos e o Cálculo de Sistemas Comunicantes - CCS) utilizem diretamente a lógica e herdem seus resultados metateóricos.

4. Resultados Chave

• Equivalência Semântica: Foi provado que a relação de satisfação indutiva coincide com a semântica denotacional ($s \models \varphi \iff s \in \llbracket \varphi \rrbracket$).
• Invariância da Bisimulação: Se dois estados são relacionados por uma bisimulação, eles satisfazem as mesmas proposições HML.
• Caracterização da Bisimilaridade (Teorema de Hennessy–Milner): Para LTSs de imagem finita (onde o conjunto de estados alcançáveis por um rótulo é finito), a equivalência teórica implica bisimilaridade. A prova deste teorema foi o ponto mais complexo, exigindo a construção de uma proposição distinguidora que combina as propriedades de todos os sucessores de um estado, explorando a finitude da imagem para garantir que a conjunção/disjunção seja finita.
• Aplicabilidade: O código foi validado aplicando-o ao formalismo CCS dentro do CSLib, demonstrando que a equivalência teórica coincide com a bisimilaridade em processos concorrentes reais definidos na biblioteca.

5. Significado e Impacto

Este trabalho representa a primeira formalização de lógica modal no CSLib, servindo como uma implementação de referência para a Lógica de Hennessy–Milner.

• Fundação para Extensões: Ao estabelecer uma base sólida e genérica, o trabalho permite futuras extensões para outras equivalências (como equivalência fraca) e operadores de ponto fixo.
• Interoperabilidade: A integração com o CSLib significa que qualquer sistema modelado usando a API de LTS da biblioteca (incluindo autômatos e processos concorrentes) pode imediatamente beneficiar-se das ferramentas de verificação e dos teoremas provados para a HML.
• Simplicidade vs. Poder: Diferente de trabalhos anteriores que formalizam extensões complexas (como sistemas de transição nominais para o $\pi$-cálculo), esta abordagem foca na simplicidade e fidelidade à HML original, provando a metateoria completa de forma genérica, o que é um passo crucial para a padronização de verificações formais em ciência da computação.

Em suma, o artigo fornece uma base robusta, reutilizável e mecanicamente verificada para o raciocínio lógico sobre sistemas de transição, preenchendo uma lacuna crítica na infraestrutura de formalização da ciência da computação no ecossistema Lean.