Computing Distinguishing Formulae for Threshold-Based Behavioural Distances

1. Problema e Motivação

Em sistemas que carregam informações quantitativas (como probabilísticas, ponderadas ou não determinísticas), as equivalências comportamentais tradicionais (de dois valores: equivalente ou não) são frequentemente insuficientes para capturar nuances finas no comportamento. As distâncias comportamentais oferecem uma alternativa mais robusta e granular, permitindo medir "quão diferente" dois estados são.

O problema central abordado pelo artigo é a caracterização lógica e a computação eficiente de fórmulas distinguidoras para uma classe específica de distâncias comportamentais chamadas distâncias baseadas em limiar (threshold-based).

• Contexto Específico: Um exemplo proeminente é a distância de $\varepsilon$-bisimulação em Cadeias de Markov, que recentemente foi mostrada como coincidindo com a distância comportamental induzida pela métrica de Lévy-Prokhorov.
• Desafio: Embora existam lógicas modais que caracterizam essas distâncias, a extração de fórmulas que provam que dois estados têm uma distância maior que um limiar $\varepsilon$ (fórmulas distinguidoras) muitas vezes carece de garantias de complexidade computacional (ex: tamanho exponencial) ou de algoritmos genéricos aplicáveis a diferentes tipos de sistemas.

2. Metodologia

Os autores desenvolvem um framework coalgebraico unificado que generaliza o tratamento de distâncias comportamentais. A abordagem baseia-se nos seguintes pilares:

• Coalgebra Universal: Os sistemas são modelados como coalgebras para um funtor $F$ sobre a categoria de conjuntos ($Set$).
• Levantamentos de Predicados (Predicate Liftings): O framework utiliza levantamentos de predicados do tipo 2-to-V (de predicados de dois valores $\{0, 1\}$ para predicados quantitativos no intervalo unitário $V = [0, 1]$). Um exemplo clássico é o operador de probabilidade, que mapeia um conjunto de estados para a probabilidade de estar nele.
• Simulações e Bisimulações $\varepsilon$: Define-se uma noção de $\varepsilon$-simulação onde as probabilidades (ou valores quantitativos) podem desviar-se em até $\varepsilon$. A distância comportamental $d_\Lambda(x, y)$ é definida como o ínfimo de todos os $\varepsilon$ para os quais $x$ e $y$ são $\varepsilon$-similares.
• Jogos de Codensidade (Codensity Games): Para computar as fórmulas distinguidoras, os autores introduzem um jogo Spoiler-Duplicator (inspirado em jogos de bisimulação) adaptado para o contexto de limiares quantitativos. O Spoiler tenta provar que a distância é maior que $\varepsilon$, enquanto o Duplicador tenta manter a similaridade.
• Construção de Modalidades Sugeno: Para a lógica quantitativa, os autores transformam os levantamentos 2-to-V em levantamentos V-to-V (quantitativos) utilizando a integração de Sugeno. Isso gera as chamadas "modalidades Sugeno".

3. Principais Contribuições e Resultados

O artigo apresenta quatro resultados teóricos e algorítmicos principais:

A. Equivalência entre Distâncias (Teorema 3.9)

Os autores provam que a distância comportamental induzida pela noção de $\varepsilon$-simulação coincide exatamente com a distância induzida por uma extensão laxa quantitativa específica (denotada por $L_\Lambda$) construída a partir dos levantamentos de predicados 2-to-V.

• Significado: Isso generaliza resultados recentes que mostraram que a distância $\varepsilon$ em Cadeias de Markov é a métrica de Lévy-Prokhorov.

B. Caracterização Lógica (Teoremas 5.8 e 6.10)

O framework estabelece dois tipos de lógicas modais que caracterizam a distância comportamental em sistemas de ramificação finita:

1. Lógica de Dois Valores com Satisfação até $\varepsilon$: Uma lógica clássica onde a satisfação de uma fórmula é relaxada pelo limiar $\varepsilon$.
2. Lógica Modal Quantitativa (Sugeno): Uma lógica onde os operadores são as modalidades Sugeno.

• Resultado: Em ambos os casos, a distância lógica (supremo das diferenças de verdade entre fórmulas) coincide com a distância comportamental. Isso constitui um teorema de Hennessy-Milner quantitativo para este contexto.

C. Extração de Fórmulas Distinguidoras em Tempo Polinomial (Teoremas 5.9 e 6.13)

Este é o resultado algorítmico central. Os autores apresentam algoritmos que extraem fórmulas distinguidoras a partir das estratégias vencedoras do Spoiler no jogo de codensidade.

• Complexidade: As fórmulas extraídas têm tamanho de DAG (Directed Acyclic Graph) polinomial (especificamente quártico) e rank modal quadrático.
• Tempo de Execução: Sob condições moderadas (se os levantamentos de predicados são "solúveis em tempo polinomial"), a extração das fórmulas e o cálculo da distância são realizados em tempo polinomial.
• Nota: Isso é uma melhoria significativa, pois em lógicas modais padrão, o tamanho da árvore das fórmulas distinguidoras pode ser exponencial.

D. Generalização de Casos Específicos

O framework unifica e gera novos resultados para vários sistemas conhecidos:

• Cadeias de Markov (Labelled): Recupera e melhora resultados sobre a distância de Lévy-Prokhorov, fornecendo extração polinomial para lógicas de dois valores e quantitativas (usando a modaliade "generally").
• Sistemas de Transição Probabilísticos Generativos.
• Sistemas de Transição Fuzzy: Recupera a lógica do diamante fuzzy.
• Sistemas de Transição Métricos: Recupera resultados sobre distâncias em sistemas com rótulos métricos.

4. Significado e Impacto

• Unificação Teórica: O trabalho fornece uma base coalgebraica sólida que unifica diversas noções de distância comportamental (Lévy-Prokhorov, Hausdorff, distâncias em sistemas fuzzy) sob um único guarda-chuva de "distâncias baseadas em limiar".
• Avanço Algorítmico: A principal contribuição prática é a demonstração de que é possível computar fórmulas distinguidoras em tempo polinomial para uma classe ampla de sistemas quantitativos. Isso é crucial para ferramentas de verificação formal, onde a explicação de por que dois estados são diferentes (através de uma fórmula) é tão importante quanto a detecção da diferença.
• Novos Resultados: Enquanto alguns casos (como sistemas métricos) já tinham algoritmos conhecidos, a aplicação a Cadeias de Markov (distância de Lévy-Prokhorov) e sistemas fuzzy através deste framework genérico representa resultados novos e significativos, especialmente a garantia de complexidade polinomial para a extração de fórmulas quantitativas.
• Aplicações Futuras: O framework abre caminho para o desenvolvimento de algoritmos genéricos de raciocínio (model checking) para lógicas modais quantitativas e para a extensão do estudo para outras relações comportamentais além de distâncias (como quasi-uniformidades).

Em resumo, o artigo resolve o problema de como caracterizar e computar eficientemente diferenças comportamentais em sistemas quantitativos complexos, oferecendo uma ferramenta teórica e algorítmica robusta que supera limitações de tamanho exponencial encontradas em abordagens anteriores.