Robust Verification of Controllers under State Uncertainty via Hamilton-Jacobi Reachability Analysis

Título: Verificação Robusta de Controladores sob Incerteza de Estado via Análise de Alcance Hamilton-Jacobi

1. O Problema

Com o aumento da adoção de controladores baseados em percepção (usando redes neurais, sensores de imagem, etc.) em sistemas autônomos, surge um desafio crítico: como garantir formalmente a segurança e o desempenho desses sistemas na presença de incerteza perceptual?

• Incerteza Perceptual: Deriva de ruído de sensores, erros de aprendizado em módulos baseados em dados (como redes neurais) e fatores ambientais (ex: bloqueio de sinal GPS).
• Desafio Atual: Métodos de verificação existentes frequentemente utilizam métodos de alcance aproximados (como conjuntos de hipercubos, zonótopos ou poliedros) que, devido à complexidade de propagar esses conjuntos em sistemas não lineares, resultam em análises excessivamente conservadoras. Isso significa que sistemas seguros podem ser erroneamente classificados como inseguros, ou falhas podem não ser detectadas.
• Limitação da Abordagem Clássica: A análise de alcance Hamilton-Jacobi (HJ) tradicional assume que o controlador tem acesso ao estado real do sistema. Quando há incerteza perceptual (o controlador usa uma estimativa $\hat{x}$ em vez de $x$), essa suposição é violada, tornando a aplicação direta da teoria HJ clássica impossível.

2. Metodologia: Framework RoVer-CoRe

Os autores propõem o RoVer-CoRe (Robust Verification of Controllers via HJ Reachability), o primeiro framework baseado em HJ para verificar sistemas baseados em percepção sob incerteza.

Abstração do Sistema em Malha Fechada:
A ideia central é concatenar o controlador ($\pi$), a função de observação ($p$) e o módulo de estimativa de estado ($q$) para formar uma dinâmica de malha fechada equivalente:
$$h(x, d, e) := f(x, \pi(q(p(x), e)), d)$$
Onde:

• $x$: Estado real.
• $e$: Sinal de erro perceptual (adversário).
• $d$: Distúrbio do sistema.
• $\hat{x} = q(p(x), e)$: Estado estimado.

Nesta abstração, a única entrada externa é a incerteza (erro $e$ e distúrbio $d$), permitindo o uso de ferramentas de alcance HJ existentes.

Cálculo do Hamiltoniano:
O principal obstáculo técnico é calcular o Hamiltoniano do sistema em malha fechada, que se torna uma função não convexa devido à complexidade do controlador e do estimador. O RoVer-CoRe propõe duas abordagens para lidar com isso:

1. Cálculo Exato: Para controladores simples ou enumeráveis (ex: controladores lineares ou baseados em grade), o problema de otimização no Hamiltoniano é resolvido exatamente. Isso fornece garantias de segurança sem conservadorismo adicional.
2. Limitação Inferior (Lower Bounding): Para controladores complexos (ex: Redes Neurais), onde o cálculo exato é inviável, o framework calcula um limite inferior do Hamiltoniano.
   • Assume-se que a estimativa de estado é uma perturbação aditiva limitada: $\hat{x} = x + e$.
   • Calculam-se limites superior e inferior para a saída do controlador ($\underline{u}(x) \leq \pi(\hat{x}) \leq \overline{u}(x)$) usando ferramentas de verificação de NN (como $\alpha,\beta$-CROWN).
   • O Hamiltoniano é limitado inferiormente considerando o pior caso dentro desses limites de controle. Isso resulta em uma verificação conservadora, mas sólida (sound).

Projeto de Controlador Robusto:
O framework também suporta o projeto de controladores. Ao parametrizar o controlador com hiperparâmetros $\alpha$, o RoVer-CoRe pode otimizar esses parâmetros para maximizar a margem de segurança ou o volume do conjunto seguro, guiando o design para regiões que resistem a erros perceptuais.

3. Contribuições Principais

1. Framework RoVer-CoRe: A primeira estrutura baseada em alcance HJ para verificação formal de sistemas baseados em percepção sob incerteza.
2. Novos Métodos de Verificação: Técnicas para calcular ou limitar o Hamiltoniano de malha fechada, permitindo a aplicação de HJ a controladores não lineares e "caixa-preta".
3. Projeto Robusto: Uma metodologia para otimizar controladores com base em garantias de segurança formal sob incerteza.
4. Validação Empírica: Demonstração da eficácia em estudos de caso reais, com código aberto.

4. Resultados nos Estudos de Caso

Caso 1: Taxiamento de Aeronaves

• Cenário: Um avião segue uma linha central usando uma câmera e uma Rede Neural (DNN) para estimar erros de posição e rumo.
• Verificação: O framework verificou a segurança do sistema para coberturas de erro de até 99,68%.
• Design: O framework identificou que o controlador original era inseguro sob certos erros e sugeriu novos ganhos (hiperparâmetros) que mantinham o avião seguro.
• Diagnóstico: O método identificou modos de falha específicos (ex: ganho excessivo de erro lateral causando correção excessiva).

Caso 2: Navegação de Rover Lunar (NASA)

• Cenário: Um rover navega em ambiente lunar com pouca luz, onde a incerteza da odometria visual cresce linearmente com o tempo. Acender as luzes reduz a incerteza, mas consome energia.
• Comparação: O RoVer-CoRe foi comparado com um controlador MPC (baseado em grade) e uma Rede Neural que imita o MPC.
• Eficiência: O método produziu garantias de segurança sólidas em ~20 segundos (GPU), enquanto simulações de Monte Carlo falharam em identificar muitos estados inseguros e ferramentas baseadas em conjuntos (NNV 2.0) foram excessivamente conservadoras.
• Política de Controle: O framework gerou uma política de ativação de luzes que garante segurança formal, acendendo as luzes apenas quando a incerteza acumulada ameaça a segurança, economizando energia.

5. Significado e Conclusão

O trabalho representa um avanço significativo na verificação formal de sistemas autônomos.

• Menor Conservadorismo: Ao substituir métodos de propagação de conjuntos aproximados pela análise HJ (que calcula conjuntos de alcance ótimos), o RoVer-CoRe fornece garantias de segurança muito mais precisas e menos conservadoras do que as ferramentas atuais.
• Ponte entre Percepção e Controle: O framework unifica a percepção, a estimativa e o controle em uma única abstração matemática tratável, permitindo analisar o impacto direto de erros de percepção na segurança global.
• Aplicabilidade Prática: Além de verificar, o framework auxilia no design de controladores mais robustos, oferecendo insights diagnósticos sobre por que um sistema falha sob incerteza.

Em resumo, o RoVer-CoRe oferece uma ferramenta rigorosa para garantir que sistemas autônomos complexos e baseados em aprendizado de máquina operem com segurança mesmo quando seus sensores e estimadores falham ou são imperfeitos.