Resumo Técnico: Uppaal Coshy – Síntese Automática de Escudos Compactos para Sistemas Híbridos

1. Definição do Problema

O artigo aborda o desafio de sintetizar estratégias de segurança (escudos/shields) para Processos de Decisão de Markov (MDPs) sobre espaços de estados contínuos com dinâmicas híbridas complexas. Diferente dos espaços de estados discretos, onde a síntese de escudos é bem estabelecida, os sistemas híbridos apresentam dificuldades algorítmicas, particularmente no que diz respeito à análise de alcançabilidade para dinâmicas não lineares e ao gerenciamento de espaços de estados infinitos.

Um gargalo prático primário identificado é a escalabilidade e o armazenamento dos escudos sintetizados. As abordagens tradicionais baseadas em partição armazenam ações permitidas para cada célula individual em uma grade, resultando em estruturas de dados massivas que são ineficientes para armazenamento e implantação, especialmente em dispositivos embarcados. Além disso, determinar células seguras e transições em sistemas híbridos gerais frequentemente envolve problemas de alcançabilidade indecidíveis.

2. Metodologia

Os autores apresentam o Uppaal Coshy, uma ferramenta totalmente integrada ao ambiente de modelagem Uppaal. A metodologia combina um algoritmo de síntese baseado em partição com aproximações baseadas em simulação e uma nova técnica de compressão.

2.1 Síntese de Escudo Baseada em Partição

O algoritmo central abstrai o espaço de estados contínuo $S \subseteq \mathbb{R}^k$ em um conjunto finito de células retangulares disjuntas usando uma grade regular definida por um vetor de granularidade $\gamma$ e um deslocamento $\omega$.

• Formulação do Jogo de Segurança: A síntese é formulada como um jogo de segurança de dois jogadores. O objetivo é computar o conjunto maximal de "células seguras" ($C_\phi$) das quais o sistema pode permanecer dentro de uma propriedade de segurança $\phi$ indefinidamente.
• Aproximação via Simulação: Como a alcançabilidade exata é frequentemente indecidível para sistemas híbridos gerais, a ferramenta emprega uma abordagem baseada em simulação:
  • Células Inicialmente Seguras ($C^0_\phi$): Em vez de raciocínio simbólico, a ferramenta amostra sistematicamente pontos dentro de cada célula. Uma célula é considerada inicialmente segura apenas se todos os pontos amostrados satisfizerem a especificação de segurança.
  • Relação de Transição: Para determinar se uma transição existe entre células ($C \xrightarrow{a} C'$), a ferramenta simula as dinâmicas do sistema a partir de estados amostrados em $C$ usando a ação $a$. Se a simulação atingir um estado onde o controlador deve fazer uma nova escolha, a célula alvo correspondente é adicionada à relação de transição.
  • Estocasticidade: Ao contrário de trabalhos anteriores que exigiam a criação manual de amostragem para dimensões estocásticas, o Uppaal Coshy permite que o simulador amostre diretamente de distribuições estocásticas, suportando distribuições gerais com suporte ilimitado.

2.2 Lidando com Desafios Práticos

• Espaços de Estados Não Limitados: A ferramenta lida com sistemas onde os limites dos estados não estão imediatamente claros (ex: uma bola saltitante) introduzindo uma célula fictícia "fora dos limites" ($C_{out}$). Os usuários podem configurar se sair dos limites é seguro, inseguro ou determinado via amostragem.
• Omissão de Variáveis: Para reduzir a dimensionalidade, os usuários podem omitir variáveis (ex: contadores de custo ou relógios) da partição da grade. Essas variáveis são fixadas em seus valores iniciais durante a síntese, desde que não influenciem a lógica de segurança.

2.3 Representação Compacta: O Algoritmo Caap

Para abordar a ineficiência de armazenamento dos escudos baseados em grade, os autores introduzem o Caap (Coarsify Axis-Aligned Partitionings).

• Objetivo: Transformar um escudo baseado em grade de granularidade fina e alinhado aos eixos em uma árvore de decisão compacta e equivalente.
• Mecanismo: O algoritmo funde iterativamente células vizinhas que compartilham o mesmo conjunto de ações permitidas em "regiões" retangulares maiores.
• Restrições: As fusões estão sujeitas a três regras de expansão para garantir que a partição resultante permaneça válida:
  1. Todas as células na nova região devem ter o mesmo conjunto de ações.
  2. A nova região não deve interceptar regiões existentes na nova partição.
  3. A expansão não deve cortar nenhuma região original em fragmentos não retangulares.
• Resultado: Isso gera uma árvore de decisão onde os nós internos representam predicados alinhados aos eixos ($s_i < c$) e as folhas representam conjuntos de ações permitidas, reduzindo significativamente o tamanho da representação.

3. Principais Contribuições

1. Ferramenta Uppaal Coshy: Uma ferramenta totalmente automática para síntese de escudo no Uppaal, suportando formalismos expressivos incluindo autômatos híbridos estocásticos e chamadas de biblioteca C externa. Ela se integra ao Uppaal Stratego para permitir o aprendizado por reforço sob um escudo sintetizado.
2. Algoritmo Caap: Um algoritmo inovador para comprimir escudos baseados em grade em árvores de decisão, preservando a funcionalidade enquanto reduz drasticamente o tamanho.
3. Aproximação Baseada em Simulação: Uma estratégia de implementação prática que evita problemas de alcançabilidade indecidíveis usando amostragem sistemática e simulação, suportando controle não periódico e distribuições estocásticas gerais.

4. Resultados e Avaliação

Os autores avaliaram a ferramenta em quatro modelos: uma bola saltitante (bouncing ball), um conversor boost, um passeio aleatório (random walk) e um tanque de água.

• Síntese e Redução: A Tabela 2 no artigo demonstra reduções significativas no tamanho do escudo. Para o modelo da bola saltitante, o escudo foi reduzido de 1.430.000 células para 2.972 regiões (um fator de redução de ~480x) em 53 segundos. O conversor boost viu uma redução de 136.800 para 571 regiões.
• Verificação de Segurança: Todos os escudos sintetizados foram avaliados estatisticamente com intervalos de confiança de 99% ao longo de 10.000 execuções. Nenhuma execução insegura foi observada, confirmando que os escudos mantiveram as propriedades de segurança (ex: impedindo que a bola pare ou que a voltagem exceda os limites).
• Demonstração de Fluxo de Trabalho: O estudo de caso da bola saltitante (Seção 5.1) ilustra um fluxo de trabalho completo: sintetizando uma estratégia básica "eficiente" (que falha na segurança), gerando um escudo, comprimindo-o via Caap e, finalmente, usando o Uppaal Stratego para aprender uma estratégia próxima da ótima sob o escudo compacto. A estratégia resultante foi tanto segura quanto eficiente.

5. Significância e Alegações

O artigo posiciona o Uppaal Coshy como uma ponte entre a síntese de escudos teórica e a aplicação prática em sistemas híbridos complexos.

• Expressividade: A ferramenta afirma lidar com uma classe de modelos mais rica do que as ferramentas existentes (como Tempest ou Uppaal Tiga), suportando especificamente sistemas híbridos estocásticos com controle não periódico e integração de código externo.
• Capacidade de Implantação: Ao introduzir o algoritmo Caap, os autores afirmam resolver o problema crítico do tamanho do escudo, tornando a implantação de estratégias sintetizadas em dispositivos embarcados com recursos limitados viável.
• Integração: A integração perfeita com o Uppaal Stratego permite um fluxo de trabalho onde a segurança é garantida pelo escudo, enquanto o desempenho é otimizado via aprendizado por reforço, uma capacidade que os autores destacam como um benefício distinto em relação ao trabalho anterior.

Os autores permanecem modestos quanto à natureza de aproximação de sua abordagem, observando que a subaproximação baseada em simulação depende do número de amostras ($n$) e das execuções de reamostragem ($m$) para se aproximar da solução real, e que o algoritmo Caap é atualmente uma ferramenta independente que eles propõem integrar diretamente na interface do usuário do Uppaal em trabalhos futuros.