Resumo Técnico: Verificação Estatística de Modelos Multiobjetivo usando Amostragem de Estratégias Leves

Declaração do Problema

A Verificação Estatística de Modelos (SMC - Statistical Model Checking) é uma técnica bem estabelecida para verificar sistemas probabilísticos com grandes espaços de estados onde a Verificação de Modelos Probabilísticos (PMC) exaustiva falha devido à explosão do espaço de estados. No entanto, as abordagens de SMC existentes são limitadas à avaliação de propriedades únicas por vez. Em muitos cenários práticos, como o equilíbrio entre o uso da bateria de um satélite e sua utilidade ou a otimização do custo de uma bomba de calor versus o conforto, os tomadores de decisão requerem a fronteira de Pareto: o conjunto de trocas (trade-offs) ótimas entre múltiplos objetivos, frequentemente conflitantes.

Embora existam algoritmos de PMC multiobjetivo (por exemplo, usando programação linear ou iteração de valor), eles exigem a exploração total do espaço de estados, tornando-os inaplicáveis a modelos com bilhões de estados ou espaços de objetivos de alta dimensão. Além disso, ferramentas existentes como o Uppaal Stratego lidam com problemas multiobjetivo apenas via ordenação lexicográfica ou otimização unidimensional, falhando em capturar as trocas entre objetivos de prioridade igual. Não há atualmente uma abordagem de SMC capaz de computar fronteiras de Pareto para consultas multiobjetivo mantendo a pegada de memória constante característica do SMC.

Metodologia

O artigo propõe a primeira abordagem de SMC para consultas de Pareto multiobjetivo, construída sobre a Amostragem de Estratégias Leves (LSS - Lightweight Strategy Sampling). A metodologia central envolve os seguintes componentes:

1. Amostragem de Estratégias Leves (LSS)

Para lidar com o não-determinismo em Processos de Decisão de Markov (MDPs) sem armazenar informações de estratégia por estado, os autores utilizam LSS. Em vez de armazenar explicitamente uma estratégia, o LSS utiliza um identificador compacto (por exemplo, um inteiro de 32 bits) e uma função de hash para resolver deterministicamente as escolhas não-determinísticas durante a simulação. Isso permite a simulação de um vasto número de estratégias distintas usando memória constante, independente do tamanho do espaço de estados do modelo.

2. Aproximação Estatística da Fronteira de Pareto

A abordagem amostra estratégias determinísticas e as avalia via SMC para obter intervalos de confiança (CIs) para cada objetivo.

• Caixas de Confiança: Para uma estratégia $\sigma$ amostrada, o SMC produz uma caixa de confiança $d$-dimensional $B_\sigma$ ao redor do vetor de média estimada $\hat{x}_\sigma$.
• Subaproximação e Sobreaproximação: O invólucro convexo dos cantos "mais pessimistas" dessas caixas forma uma subaproximação ($\underline{C}$) candidata do conjunto alcançável. Inversamente, os cantos "mais otimistas" formam uma sobreaproximação ($\overline{C}$) candidata.
• Múltiplas Comparações: Para garantir a correção simultânea de todas as caixas de confiança com probabilidade $\gamma$, os autores aplicam a correção de Bonferroni (limite da união) para distribuir o orçamento de erro entre estratégias e dimensões.

3. Algoritmos

O artigo introduz duas categorias de algoritmos:

A. Amostragem Incremental com Convergência
Este esquema amostra lotes de estratégias indefinidamente. Ele ajusta dinamicamente o orçamento de erro por lote (usando um fator $f$) para garantir que, no limite, as sub e sobreaproximações convirjam para uma banda de confiança simultânea em torno da verdadeira fronteira de Pareto. Isso fornece uma garantia teórica de convergência quase certa dado um LSS ideal.

B. Amostragem de Orçamento Fixo
Reconhecendo que aplicações práticas possuem tempo finito, três algoritmos heurísticos são propostos para encontrar a melhor aproximação dentro de um orçamento de simulação fixo:

1. Refinamento de Vetor de Peso (WVR): Adapta técnicas de PMC multiobjetivo através da escalarização linear dos objetivos. Ele refina iterativamente os vetores de peso com base na distância entre as aproximações atuais e descarta estratégias subótimas.
2. Orçamento de Iteração Fixa (FIB): Amostra um conjunto inicial de estratégias e realiza execuções iterativas, descartando as estratégias de pior desempenho em cada iteração para concentrar o orçamento em candidatos promissores.
3. Orçamento de Estratégia Fixa (FSB): Semelhante ao FIB, mas garante que o conjunto final de estratégias sobreviventes receba um número uniforme de execuções de simulação, amostrando novas estratégias para substituir as descartadas.

Heurísticas de Seleção de Estratégia:
Para filtrar estratégias, os autores definem várias regras baseadas em médias de amostra e intervalos de confiança (ex: "Simples", "Suficientemente Longe", "Conservadoramente Longe"). Essas regras determinam se uma estratégia é dominada por outra com confiança estatística suficiente para ser descartada.

Principais Contribuições

1. Primeiro SMC Multiobjetivo: O artigo apresenta o primeiro framework de SMC capaz de aproximar fronteiras de Pareto para $d$ objetivos de igual prioridade.
2. Memória Constante: A abordagem mantém a principal vantagem do SMC: o uso de memória é constante em relação ao tamanho do espaço de estados do modelo, permitindo a análise de modelos com bilhões de estados.
3. Garantias Estatísticas: O esquema incremental fornece uma garantia teórica de convergência para uma banda de confiança em torno da verdadeira fronteira de Pareto. Os algoritmos de orçamento fixo fornecem limites inferiores estatisticamente válidos (subaproximações) com um nível de confiança especificado.
4. Implementação e Avaliação: As técnicas são implementadas no simulador modes dentro do Modest Toolset. Os autores avaliam a abordagem em 40 instâncias de benchmark da literatura de verificação quantitativa e aprendizado por reforço, comparando os resultados com a ferramenta de PMC Storm.

Resultados Experimentais

Os experimentos demonstram que a proposta de SMC pode lidar com instâncias onde as ferramentas de PMC (Storm) falham devido à explosão do espaço de estados ou tempo esgotado (timeout).

• Escalabilidade: Para modelos grandes (ex: fruit_tree com $2.7 \times 10^9$ estados, variantes de puddle_world com centenas de milhões de estados), a abordagem de SMC consegue computar aproximações da fronteira de Pareto em segundos ou minutos, enquanto as ferramentas de PMC sofreram timeout ou não puderam completar.
• Precisão: Para modelos menores onde os resultados de PMC estão disponíveis, as aproximações de SMC frequentemente coincidem de perto com a verdadeira fronteira de Pareto (ex: modelos deep_sea e fruit_tree com $\epsilon$ multiplicativo próximo de 1). No entanto, a precisão varia; para alguns modelos como breakable_bottles, a aproximação pode estar mais distante da fronte verdade, destacando a natureza estocástica da amostragem.
• Desempenho dos Algoritmos: Entre os algoritmos de orçamento fixo, o FSB (Orçamento de Estratégia Fixa) combinado com a heurística Simple e uma configuração que favorece um alto número de estratégias iniciais com menos execuções por estratégia, geralmente apresentou os melhores resultados de hipervolume.
• Impacto da Heurística: A regra "Simple" (descartar estratégias baseando-se puramente nas médias das amostras) frequentemente performou melhor, sugerindo que o descarte precoce de estratégias não promissoras é benéfico no conjunto de benchmarks testado.

Significância e Alegações

Os autores afirmam que este trabalho preenche uma lacuna crítica entre a escalabilidade do SMC e a complexidade da otimização multiobjetivo. Ao utilizar a amostragem de estratégias leves, a abordagem permite a verificação de trocas em sistemas que seriam de outra forma intratáveis para métodos exaustivos.

O artigo reconhece modestamente as limitações:

• Sobreaproximação: Embora o esquema incremental convirja para uma banda de confiança, os algoritmos de orçamento fixo não podem garantir uma sobreaproximação válida em tempo finito porque podem perder a estratégia ótima.
• Espaço de Estratégias: O método assume um espaço de estratégias finito (via identificadores de tamanho fixo). Embora prático, isso é uma limitação em comparação ao espaço teórico infinito de estratégias em MDPs gerais.
• Classe de Modelo: Embora demonstrado em MDPs, a abordagem é diretamente aplicável a qualquer classe de modelo suportada por LSS, como autômatos de Markov e autômatos temporais probabilísticos, desde que as execuções terminem quase certamente.

O trabalho é apresentado como um passo fundamental, oferecendo uma ferramenta prática para a verificação multiobjetivo em sistemas de grande escala onde os métodos tradicionais exaustivos não estão disponíveis.