Resumo Técnico: Bisimilaridade Probabilística Robusta para Cadeias de Markov Rotuladas

Declaração do Problema

A bisimilaridade probabilística é um conceito fundamental na verificação de sistemas probabilísticos, permitindo a minimização de espaços de estados ao fundir estados comportamentalmente indistinguíveis. No entanto, a bisimilaridade probabilística padrão carece de robustez sob pequenas perturbações das probabilidades de transição. Embora a função de distância de bisimilaridade probabilística (uma pseudométrica comportamental) quantifique a similaridade entre estados, ela é frequentemente descontínua. Isso significa que mudanças arbitrariamente pequenas nas probabilidades de transição podem fazer com que a distância entre dois estados salte abruptamente de 0 (bisimilares) para um valor grande (ex: 1), ou vice-versa.

Esta descontinuidade impõe um problema significativo de confiabilidade em aplicações práticas onde as probabilidades de transição são derivadas de dados experimentais e são, inerentemente, aproximadas. Como ilustrado pelos exemplos do artigo, dois estados podem ser bisimilares em um modelo nominal ($\varepsilon = 0$), mas exibir comportamentos de longo prazo maximamente diferentes (ex: propriedades de alcançabilidade) sob perturbações infinitesimais ($\varepsilon > 0$). Consequentemente, fundir tais estados em um modelo minimizado pode ser inseguro se as probabilidades de transição precisas forem desconhecidas.

Metodologia

Os autores introduzem a bisimilaridade probabilística robusta ($\simeq$) como um subconjunto mais estrito da bisimilaridade probabilística padrão ($\sim$). A metodologia central envolve:

1. Caracterização Baseada em Políticas: O artigo utiliza o conceito de políticas (acoplamentos) no espaço de produto de estados $S \times S$. Uma política $P$ mapeia pares de estados para distribuições sobre $S \times S$.
2. Definição de Robustez: Dois estados $s$ e $t$ são robustamente bisimilares ($s \simeq t$) se existir uma política $P$ tal que o par $(s, t)$ atinja o conjunto diagonal $S^2_\Delta = \{(s, s) \mid s \in S\}$ com probabilidade 1 na cadeia de Markov induzida $\langle S \times S, P \rangle$.
3. Garantia de Continuidade: Os autores provam que, se $s \simeq t$, a função de distância de bisimilaridade probabilística $\delta(s, t)$ é contínua em relação a perturbações da função de transição $\tau$. Especificamente, para qualquer sequência de funções de transição $\tau_n$ convergindo para $\tau$, se $s \simeq t$, então $\lim_{n \to \infty} \delta_{\tau_n}(s, t) = 0$. Isso contrasta com a bisimilaridade padrão, onde o limite pode não ser igual à distância no ponto nominal.
4. Computação Algorítmica: O artigo apresenta um algoritmo de tempo polinomial (Algoritmo 1) para computar a maior bisimilaridade robusta. O algoritmo refina iterativamente um conjunto inicial de estados bisimilares usando três funções:
   • Filter (Filtro): Identifica pares que podem alcançar a diagonal $S^2_\Delta$ sob alguma política suportada pela relação atual.
   • Prune (Poda): Garante que a relação permaneça simétrica e transitiva em relação ao "vizinhança" definida pelo passo de Filtro.
   • Bisim: Computa a maior bisimilaridade contida dentro da relação atual.
     O algoritmo termina no maior ponto fixo da composição dessas funções.

Principais Contribuições

• Definição Formal: A introdução da bisimilaridade probabilística robusta, definida via políticas que garantem o alcance quase certo da diagonal no espaço de produto.
• Garantia Teórica: Uma prova (Teorema 2) de que a bisimilaridade probabilística robusta é uma condição suficiente para a continuidade da função de distância de bisimilaridade probabilística sob perturbações arbitrárias das probabilidades de transição.
• Algoritmo Eficiente: O desenvolvimento de um algoritmo $O(n^6)$ (onde $n$ é o número de estados) para computar a bisimilaridade probabilística robusta, tornando-o viável para tarefas de verificação em larga escala.
• Validação Empírica: Implementação do algoritmo no model checker PRISM e avaliação em benchmarks do Conjunto de Benchmark de Verificação Quantitativa (QVBS) e da extensão jpf-probabilistic.

Resultados Experimentais

Os autores avaliaram sua implementação contra 170 modelos. As principais descobertas incluem:

• Viabilidade: A bisimilaridade robusta foi computada com sucesso para 152 modelos (aprox. 89%) em menos de um minuto.
• Diferenças de Espaço de Estados: Nos casos em que os modelos minimizados diferiram, a abordagem robusta resultou frequentemente em espaços de estados significativamente maiores em comparação com a bisimilaridade tradicional, identificando corretamente pares de estados que não devem ser fundidos devido à sensibilidade.
• Sobrecarga de Desempenho: Embora a bisimilaridade robusta seja mais lenta que a bisimilaridade tradicional (com aumentos de tempo médio variando de 28% a mais de 140.000%, dependendo do benchmark, ex: o benchmark crowds), o tempo de computação permaneceu prático para a maioria dos modelos padrão.
• Limitações: Para 10 modelos (aprox. 6%), o algoritmo robusto falhou devido a restrições de memória (OutOfMemoryError), enquanto a bisimilaridade tradicional teve sucesso. Isso foi observado em instâncias específicas dos benchmarks nand e egl.

Significância e Alegações

O artigo afirma que a bisimilaridade probabilística robusta fornece um método mais confiável para determinar a equivalência de estados em sistemas probabilísticos onde as probabilidades de transição são aproximações. Ao garantir a continuidade da função de distância, a abordagem mitiga o risco de fundir estados que se comportam de maneira diferente sob pequenas variações de parâmetros.

Os autores posicionam este trabalho como um passo necessário para aplicações práticas, particularmente em sistemas de missão crítica que exigem alta precisão. Eles observam que, embora a bisimilaridade robusta seja uma condição suficiente para a continuidade, eles conjecturam que ela também possa ser uma condição necessária para estados bisimilares. O artigo conclui identificando direções futuras, incluindo caracterizações lógicas da bisimilaridade robusta e investigação de tipos específicos de perturbações que preservam a estrutura do grafo versus aquelas que introduzem novas transições.