Computing Sound Lower and Upper Bounds on Hamilton-Jacobi Reach-Avoid Value Functions

Resumo Técnico: Cálculo de Limites Inferiores e Superiores Sólidos para Funções de Valor de Hamilton-Jacobi

1. Problema e Motivação

A análise de alcançabilidade de Hamilton-Jacobi (HJ) é uma ferramenta fundamental para verificação de segurança e síntese de controle em sistemas não lineares. O objetivo é determinar o Conjunto de Alcançabilidade Reversa (BRS) (estados de onde é impossível evitar um conjunto de falha) e o Conjunto de Alcançabilidade-Avoid (RAS) (estados de onde é possível atingir um alvo evitando falhas).

O problema central abordado pelo artigo é a incerteza devido à discretização. Métodos clássicos de HJ resolvem equações diferenciais parciais (EDP) em grades (grids) discretas do espaço de estados contínuo. No entanto:

• Eles geralmente não contabilizam explicitamente os erros de discretização.
• Não garantem que os conjuntos computados sejam super-approximações sólidas do BRS (garantindo que nenhum estado inseguro seja classificado erroneamente como seguro) ou sub-approximações sólidas do RAS (garantindo que nenhum estado seguro seja classificado erroneamente como inseguro).
• Métodos existentes frequentemente param a iteração de valor antes da convergência exata, introduzindo erros adicionais que comprometem a garantia de segurança.

2. Metodologia Proposta

Os autores propõem um framework que calcula limites inferiores e superiores sólidos para a função de valor de HJ, garantindo aproximações conservadoras e rigorosas.

A. Abstração Discreta e Limites de Célula:

• O espaço de estados contínuo é discretizado em uma grade finita de células.
• Para cada célula, são calculados limites superiores e inferiores para as funções de falha ($l$) e recompensa ($r$), utilizando as constantes de Lipschitz dessas funções e o tamanho da célula. Isso cria uma "caixa" de valores possíveis para qualquer estado dentro da célula.

B. Duas Funções de Valor Discretas:
Em vez de calcular uma única função de valor aproximada, o algoritmo calcula duas funções sobre a grade discreta:

1. $V^\gamma$ (Limitante Superior): Representa o melhor cenário possível (melhor política e melhor trajetória dentro da incerteza da célula). Garante que, se $V^\gamma(s) \le 0$, então todo o estado na célula $s$ pertence ao conjunto de falha (BRS).
2. $V_\gamma$ (Limitante Inferior): Representa o pior cenário possível (pior trajetória dentro da incerteza). Garante que, se $V_\gamma(s) > 0$, então todo o estado na célula $s$ pertence ao conjunto de alcançabilidade segura (RAS).

C. Tratamento da Parada Antecipada (Early Stopping):
Um dos principais desafios é a convergência da iteração de valor. O artigo demonstra que, mesmo que a iteração seja interrompida antes de atingir o ponto fixo:

• É possível calcular um termo de correção baseado na variação mínima entre iterações ($\delta_k$).
• Para o limite inferior, aplica-se uma correção conservadora ($V_{cons} = V^{(k)} + \frac{\gamma \delta_k}{1-\gamma}$) para garantir que o valor ainda seja um limite inferior sólido.
• Para o limite superior, a sequência de iteração é monotonicamente decrescente, permitindo que o valor atual seja usado diretamente como um limite superior sólido.

D. Algoritmo de Refinamento Adaptativo (Algoritmo 2):

• Células que não podem ser classificadas definitivamente (onde o limite inferior é $\le 0$ e o superior é $> 0$) são identificadas como "não classificadas".
• O algoritmo divide recursivamente essas células ao longo de sua maior dimensão.
• As funções de valor são recomputadas na grade refinada.
• Isso resulta em uma grade não uniforme, com maior resolução apenas nas fronteiras críticas entre conjuntos seguros e inseguros, otimizando o custo computacional.

3. Contribuições Principais

1. Garantias de Sólidez (Soundness): O método fornece limites superiores e inferiores prováveis para as funções de valor de HJ, garantindo que o BRS seja super-approximado e o RAS sub-approximado, mesmo na presença de erros de discretização.
2. Robustez à Parada Antecipada: Estabelece que os limites calculados permanecem válidos e sólidos mesmo quando a iteração de valor é interrompida antes da convergência completa, algo que métodos anteriores não garantiam.
3. Refinamento Adaptativo Local: Desenvolveu um algoritmo que refina dinamicamente apenas as células ambíguas, evitando o custo computacional excessivo de grades uniformes finas em todo o espaço.
4. Análise Quantitativa: Diferente de métodos puramente simbólicos que fornecem classificações binárias (seguro/inseguro), este método fornece uma função de valor que quantifica o "margem de segurança" ou o grau de satisfação da especificação.

4. Resultados Experimentais

Os autores validaram o método em dois estudos de caso:

1. Carro de Dubins: Um modelo de veículo com dinâmica não linear em 2D.
2. Evasão 3D: Um cenário de perseguição-evasão aérea.

Comparação e Desempenho:

• Contra Toolbox HJ Existente: A toolbox clássica de HJ (baseada em EDPs contínuas) falhou em garantir a sólidez em resoluções de grade baixas, classificando erroneamente estados inseguros como seguros. O método proposto manteve a garantia de segurança em todas as resoluções.
• Contra ROCS 2.0 (Síntese Simbólica): O método proposto conseguiu calcular um conjunto de alcançabilidade (RAS) maior (menos conservador) do que o ROCS 2.0 com tempos de execução comparáveis ou menores, dependendo dos parâmetros.
• Eficiência: O algoritmo de refinamento adaptativo mostrou que o tempo de execução cresce quase linearmente com o tamanho da grade, permitindo lidar com a complexidade exponencial de forma mais eficiente ao focar apenas nas regiões de fronteira.
• Discriminação: O método conseguiu classificar corretamente células que outras ferramentas deixavam como "incertas" ou conservadoras demais.

5. Significado e Impacto

Este trabalho preenche uma lacuna crítica na verificação formal de sistemas de controle não lineares. Ao garantir que as aproximações numéricas não introduzam falsos positivos (estados inseguros considerados seguros), o método é essencial para aplicações de segurança crítica (como veículos autônomos e robótica cirúrgica).

A capacidade de fornecer limites sólidos mesmo com iteração interrompida permite um equilíbrio prático entre precisão e tempo de computação, algo vital para sistemas em tempo real. Além disso, a abordagem de refinamento adaptativo oferece uma via para lidar com a "maldição da dimensionalidade" de forma mais eficiente do que as grades uniformes tradicionais, focando o esforço computacional onde a incerteza é maior.