A Diagrammatic Axiomatisation of Behavioural Distance of Nondeterministic Processes

1. Declaração do Problema

O artigo aborda o desafio de comparar quantitativamente os comportamentos de processos não determinísticos.

• Contexto: A álgebra de processos tradicional e a teoria dos autômatos baseiam-se em noções booleanas de equivalência (por exemplo, bisimilaridade, equivalência de linguagens). Embora úteis, essas noções são frequentemente muito rígidas para sistemas modernos que envolvem aspectos probabilísticos ou quantitativos, onde é necessário medir quão distantes dois comportamentos estão, em vez de apenas verificar se são idênticos.
• Lacuna Específica: Embora distâncias comportamentais tenham sido estudadas para sistemas probabilísticos e autômatos determinísticos (DFA), há uma falta de uma estrutura axiomática sólida e completa para processos não determinísticos (especificamente os diagramas de Milner).
• Desafio: O não determinismo desloca o foco semântico da equivalência de linguagens para a bisimilaridade. Sintaxes algébricas existentes (como expressões regulares com ligadores) lutam para capturar esses comportamentos de forma composicional sem mecanismos de substituição complexos. Além disso, estender o raciocínio quantitativo para sistemas não determinísticos exige lidar com o "levantamento de Hausdorff" de métricas, o que é tecnicamente difícil de axiomatizar.

2. Metodologia

Os autores adotam uma abordagem diagramática utilizando diagramas de cordas (a linguagem gráfica das categorias monoidais simétricas) para representar e raciocinar sobre comportamentos de processos.

• Modelo Semântico (Diagramas): O artigo foca nos diagramas de Milner, que generalizam autômatos não determinísticos de estado finito (NFA) substituindo estados de aceitação por saídas variáveis. A semântica é definida sobre uma categoria de comportamentos regulares ($\Omega$), equipada com uma estrutura de pseudométrica.
• Definição de Métrica: A distância comportamental é definida através de uma estrutura coalgebraica. Ela utiliza:
  1. Levantamento de Transição: Levantar uma métrica sobre estados para uma métrica sobre transições (arestas rotuladas e saídas variáveis).
  2. Levantamento de Hausdorff: Levantar a métrica para conjuntos de transições (para lidar com o não determinismo).
  3. Caracterização de Ponto Fixo: A distância é o menor ponto fixo de um operador monótono no reticulado de pseudométricas. É concretamente caracterizada pela estratificação da bisimilaridade (lógica de Hennessy-Milner), onde a distância é $2^{-n}$ se dois processos forem bisimilares até a profundidade $n$, mas não $n+1$.
• Sintaxe (Diagramas de Cordas): Os autores utilizam diagramas de cordas como sintaxe. Essa escolha oferece:
  • Representação sem variáveis: A recursão é tratada por meio de laços de feedback (rastros) em vez de ligadores explícitos e substituição.
  • Semântica Composicional: Os diagramas mapeiam naturalmente para a estrutura categórica dos comportamentos regulares.
  • Construção Int: Para lidar com fluxo de dados bidirecional (entradas/saídas) e laços de feedback, os autores utilizam a construção Int para transformar a categoria monoidal traçada de comportamentos em uma categoria compacta fechada, permitindo a curvatura local de fios.

3. Contribuições Principais

A. Um Sistema de Inferência Quantitativo

O artigo propõe um conjunto de regras equacionais quantitativas (sistema de inferência) para derivar limites sobre distâncias comportamentais ($s \equiv_\epsilon t$).

• Regras Métricas Padrão: Reflexividade, Simetria, Desigualdade Triangular e uma regra de "Continuidade" (se $s \equiv_{\epsilon'} t$ para todo $\epsilon' > \epsilon$, então $s \equiv_\epsilon t$).
• Regras Composicionais: Regras para composição sequencial e composição paralela (tensor) que preservam a não expansão.
• Regras Específicas do Domínio:
  • (Pref): Prefixar com uma ação $a$ reduz a distância pela metade ($d(a.s, a.t) = \frac{1}{2}d(s, t)$). Isso captura a intuição de que distinguir dois processos requer mais um passo.
  • (Codel): Um diagrama sem estado inicial (deadlock) está a distância 0 do diagrama vazio.
  • Axiomas Equacionais: Um conjunto de axiomas (A1-B11) que capturam a bisimilaridade forte (distância 0), incluindo leis para escolha não determinística, mesclagem de variáveis e recursão (axiomas da teoria de Conway).

B. Solidez e Completude

A realização técnica central é a prova de que o sistema de inferência é tanto sólido quanto completo.

• Solidez (Teorema 16): Toda equação quantitativa derivável $f \equiv_\epsilon g$ é válida (ou seja, a distância comportamental real $d(\llbracket f \rrbracket, \llbracket g \rrbracket) \leq \epsilon$).
• Completude (Teorema 31): Se a distância comportamental entre dois diagramas for $\leq \epsilon$, então a equação $f \equiv_\epsilon g$ é derivável usando as regras propostas.
  • Estratégia de Prova: A prova de completude envolve transformar diagramas arbitrários em uma forma normal (representando um pré-diagrama finito). Em seguida, simula-se o cálculo do levantamento de Hausdorff e da iteração de ponto fixo (teorema de Kleene) sintaticamente usando as regras de inferência. A regra de Continuidade (Cont) é crucial para fechar a lacuna entre a aproximação sintática e o limite exato.

C. Estrutura Categórica

O artigo estabelece que a categoria de comportamentos regulares ($\text{RegBeh}$) é uma Teoria de Conway (um tipo específico de categoria monoidal traçada) e que a estrutura de pseudométrica a torna uma categoria enriquecida sobre a categoria de espaços de pseudométricas ($\text{PMet}$). Isso garante que todas as operações categóricas (composição, tensor, traço/dagger) sejam não expansivas.

4. Resultados

• Caracterização Formal: O artigo fornece a primeira axiomatização completa da distância comportamental para os diagramas de Milner (processos não determinísticos com saídas).
• Simulação Sintática de Métricas: Os autores demonstram que cálculos métricos complexos, como a distância de Hausdorff entre conjuntos de transições, podem ser simulados puramente através da manipulação sintática de diagramas de cordas.
• Exemplo de Aplicação: O artigo inclui uma derivação detalhada mostrando como provar que dois diagramas específicos (um com um deadlock após dois 'a's, e outro com 'a's infinitos) estão a uma distância exatamente de $1/4$. Isso é alcançado desdobrando a recursão e aplicando a regra (Pref) duas vezes.

5. Significado

• Ponte entre Teoria e Prática: Ao migrar da equivalência booleana para a distância quantitativa, o trabalho permite uma análise mais matizada de sistemas onde "quase equivalente" é um conceito significativo (por exemplo, na verificação de sistemas aproximados ou sistemas probabilísticos).
• Estrutura Diagramática Unificada: O uso de diagramas de cordas evita a complexidade da ligação de variáveis e da substituição encontradas em álgebras de processos tradicionais. Isso sugere um caminho para uma estrutura unificada para axiomatizar equivalências e distâncias em vários modelos computacionais (determinísticos, não determinísticos, probabilísticos, ponderados).
• Fundação para Trabalhos Futuros: O artigo estabelece as bases para estender esses resultados para sistemas de transição ponderados e autômatos probabilísticos, onde as distâncias comportamentais são ainda mais críticas. Também sugere aplicações potenciais no raciocínio sobre algoritmos de decompilação e Álgebra de Kleene Guardada com Testes (GKAT).
• Avanço Teórico: Conecta métricas comportamentais coalgebraicas, lógica equacional quantitativa e álgebra diagramática, mostrando como esses campos podem ser integrados para resolver problemas de longa data na teoria de processos.

Em resumo, este artigo traduz com sucesso a definição abstrata, coalgebraica, de distância comportamental para processos não determinísticos em um cálculo concreto, diagramático e totalmente axiomatizado, provando que o raciocínio quantitativo sobre o comportamento de processos pode ser realizado inteiramente através da manipulação sintática de diagramas de cordas.