Data-Driven Reachability of Nonlinear Lipschitz Systems via Koopman Operator Embeddings

Resumo Técnico: Análise de Alcançabilidade de Sistemas Não Lineares via Operador de Koopman

1. Problema e Motivação

A verificação de segurança em sistemas robóticos dinâmicos e incertos é fundamental. Métodos tradicionais baseados em modelos formais frequentemente falham em ambientes do mundo real devido à dificuldade de obter modelos dinâmicos precisos e caracterizações conservadoras de incertezas.

• Desafio Atual: Abordagens de análise de alcançabilidade baseadas em dados (data-driven) que utilizam representações zonotópicas são escaláveis e eficientes, mas tornam-se excessivamente conservadoras para sistemas não lineares, especialmente em horizontes de previsão longos e na presença de ruído de medição.
• Limitação das Abordagens Existentes: Métodos que tentam linearizar sistemas não lineares (como modelos LTI - Lineares Invariantes no Tempo) ou usam redes neurais como "caixas pretas" muitas vezes não garantem limites formais de segurança ou sofrem de baixa eficiência amostral e complexidade de treinamento.

2. Metodologia Proposta

O artigo apresenta um novo framework de análise de alcançabilidade baseado em dados que utiliza Operadores de Koopman para mapear sistemas não lineares não afins em um espaço de estados elevado (lifted space) de dimensão finita, onde a dinâmica evolui aproximadamente de forma linear.

Etapas Principais do Método:

1. Elevação (Lifting) Dependente de Estado e Entrada:

   • Diferente de modelos Koopman tradicionais que assumem estruturas lineares invariantes no tempo (LTI), o método propõe funções de elevação (observáveis) que dependem tanto do estado ($x$) quanto da entrada de controle ($u$).
   • Isso permite uma representação linear mais precisa da dinâmica não linear subjacente.

2. Identificação do Operador de Koopman:

   • O operador é identificado diretamente a partir de dados medidos (trajetórias de estado-entrada ruidosas) usando regressão por mínimos quadrados (Least Squares).
   • O sistema é transformado em um modelo linear discreto no espaço elevado: $z_{k+1} = A z_k + B \nu(z_k, u_k) + \text{resíduos}$.

3. Modelagem de Incertezas e Erros:
   Para garantir garantias formais de segurança (sobrecobertura garantida), o método agrega quatro fontes de incerteza em conjuntos zonotópicos:

   • Ruído do Processo: Limitado por um zonotope conhecido.
   • Erro de Linearização: O termo de resto de Taylor da linearização da dinâmica elevada é limitado.
   • Erro de Modelagem (Resíduo): Calculado agregando erros de previsão multi-passos em todas as trajetórias disponíveis no conjunto de dados.
   • Erro de Cobertura (Covering Radius): Garante que o limite de erro derivado dos dados se estenda a todo o domínio alcançável, assumindo que o sistema é Lipschitz contínuo.

4. Propagação e Projeção:

   • Os conjuntos de estados alcançáveis são propagados no espaço elevado usando somas de Minkowski e transformações lineares de zonotopos (computacionalmente eficientes).
   • Os conjuntos resultantes são projetados de volta ao espaço de estado original e combinados com os conjuntos de incerteza de modelagem para obter uma sobrecobertura garantida (over-approximation) da dinâmica não linear original.

3. Contribuições Principais

• Framework Data-Driven para Sistemas Não Afins: Introdução de um método capaz de lidar com sistemas não lineares não afins e ruidosos, sem exigir um modelo matemático prévio.
• Elevação Dependente de Estado-Entrada: Desenvolvimento de uma abordagem de identificação que utiliza observáveis dependentes de $x$ e $u$, superando a precisão dos modelos LTI elevados padrão.
• Garantias Formais Rigorosas: Prova teórica de que os conjuntos de alcançabilidade computados são superconjuntos dos conjuntos de alcançabilidade exatos ($\bar{X}_k \subseteq R'_k$), mesmo na presença de ruído e erros de aprendizado.
• Eficiência Computacional: Uso de representações zonotópicas para permitir análise escalável em horizontes de tempo longos.

4. Resultados e Validação

O método foi validado através de simulações numéricas e experimentos em um veículo autônomo real:

• Exemplo 1 (Reator CSTR): Um sistema dinâmico afim Lipschitz. O método proposto mostrou-se significativamente menos conservador do que o método CORA (baseado em modelo) e métodos de mínimos quadrados (LS) puros, especialmente em horizontes longos.
• Exemplo 2 (Sistema Não Afim): Um sistema não linear não afim complexo. Novamente, a abordagem baseada em Koopman produziu conjuntos de alcançabilidade mais apertados (tighter) do que as abordagens concorrentes.
• Exemplo 3 (Veículo Autônomo - JetRacer): Experimento em um robô de corrida real. Os resultados demonstraram que o método proposto mantém a precisão e a escalabilidade em cenários do mundo real, superando métodos baseados em dados lineares e métodos baseados em modelos tradicionais.

Comparação Visual: As figuras do artigo (Fig. 2, 3 e 5) ilustram que, enquanto os métodos tradicionais expandem rapidamente (tornando-se muito conservadores) ao longo do tempo, o método proposto mantém os conjuntos de alcançabilidade próximos à trajetória real.

5. Significado e Impacto

Este trabalho preenche uma lacuna crítica entre a identificação de sistemas baseada em dados e a verificação formal de segurança.

• Segurança Garantida: Permite que sistemas robóticos operem com garantias de segurança rigorosas mesmo quando o modelo exato é desconhecido.
• Redução de Conservadorismo: Ao capturar melhor a não linearidade através do operador de Koopman, evita-se o "excesso de proteção" que limita a performance de robôs em tarefas complexas.
• Aplicabilidade Prática: A validação em um veículo autônomo real demonstra que a teoria é aplicável a sistemas embarcados com restrições computacionais, oferecendo uma ferramenta viável para o controle e verificação de sistemas autônomos em ambientes incertos.

Em suma, o artigo oferece uma solução robusta para a verificação de segurança de sistemas não lineares, combinando a flexibilidade do aprendizado de máquina com a rigidez da análise de conjuntos formais.