TERA: A Unified Taylor Model Enabled Reachability Analysis Framework

Resumo Técnico: TERA – Um Framework de Análise de Alcançabilidade Baseado em Modelo de Taylor Unificado

Problema
A verificação de sistemas críticos de segurança, definidos por dinâmicas como $\dot{x} = f(x, u, w)$, onde $w$ representa perturbações limitadas ou incertezas, requer o cerceamento rigoroso de todas as trajetórias possíveis de estado sobre um horizonte de tempo finito. Embora o cálculo exato de flowpipes seja geralmente inviável para sistemas não lineares, sobre-aproximações baseadas em conjuntos são necessárias para a verificação de segurança. No entanto, representações tradicionais como (hiper-)intervalos e zonótopos sofrem do "efeito de embrulho" (wrapping effect), onde as sobre-aproximações acumuladas levam a cerceamentos de conjuntos alcançáveis excessivamente conservadores. Além disso, ferramentas existentes baseadas em Modelos de Taylor (TM) (ex: Flow*, CORA, JuliaReach) são frequentemente escritas em linguagens compiladas (C++, MATLAB, Julia), o que dificulta a prototipagem rápida, ou carecem de suporte para sistemas estocásticos e classes amplas de sistemas dentro de um fluxo de trabalho unificado.

Metodologia
O TERA aborda essas limitações fornecendo um framework nativo de Python que se integra ao ecossistema científico de Python e aproveita o sistema de álgebra computacional SageMath. A metodologia central baseia-se em Modelos de Taylor (TM) da forma $P(x_0, t) + I$, onde $P$ é uma aproximação polinomial de Taylor de alta ordem da solução e $I$ é um resto de intervalo que garante que a solução verdadeira esteja contida.

Os componentes metodológicos principais incluem:

• Propagação: Dinâmicas de tempo contínuo são propagadas usando esquemas de integração de TM validados, fundamentados no trabalho de Berz e Makino, juntamente com abordagens de construção de flowpipes para sistemas não lineares por Chen.
• Mitigação do Efeito de Embrulho: Para manter cerceamentos estreitos ao longo de longos horizontes de tempo, o TERA implementa a propagação composicional esquerda-direita usando o método de "encolhimento de embrulho" (shrink-wrapping).
• Suporte ao Sistema:
  • EDOs Não Lineares: Suporta sistemas com não linearidades não polinomiais (ex: funções transcendentais como $\sin$ e $\cos$).
  • Sistemas Híbridos: Computa interseções de guarda de autômatos híbridos e transições discretas seguindo a semântica de alcançabilidade híbrida baseada em TM.
  • Sistemas Estocásticos: Para sistemas estocásticos de tempo contínuo, o TERA combina flowpipes de TM determinísticos com limites de desvio probabilísticos para computar cerceamentos de conjunto alcançável $\delta$-probabilístico ($\delta$-PRS). Isso garante que as trajetórias permaneçam dentro dos conjuntos computados com uma probabilidade de pelo menos $1-\delta$.
• Aritmética Rigorosa: O arredondamento correto é alcançado via biblioteca GNU MPFR integrada ao SageMath para garantir o rigor matemático.

Principais Contribuições

1. Framework Unificado: O TERA é apresentado como o primeiro framework gratuito, de código aberto, nativo de Python, capaz de lidar com sistemas contínuos, híbridos e estocásticos dentro de um único fluxo de trabalho simbólico-numérico.
2. Extensibilidade: Ao aproveitar o Python e o SageMath, o framework facilita a prototipagem rápida de técnicas de análise de alcançabilidade, abordando a rigidez das ferramentas existentes em C++ ou MATLAB proprietário.
3. Capacidade Estocástica: O framework estende a alcançabilidade baseada em TM para sistemas estocásticos de tempo contínuo, computando cerceamentos $\delta$-PRS.
4. Disponibilidade Aberta: O software é distribuído sob a licença GPLv2 e está disponível via GitHub.

Resultos e Validação
Os autores validaram o TERA contra o conjunto de problemas de referência da competição ARCH [5]. Os resultados demonstram a capacidade do framework de computar sobre-aproximações de conjuntos alcançáveis estreitas para problemas de referência difíceis:

• Sistemas Contínuos Não Lineares: O TERA computou com sucesso um cerceamento estreito para uma rede de reação bioquímica de Laub-Loomis de 7 dimensões sobre $t \in [0, 20]$ em 13 segundos. Também escalou para um problema de quadrotor controlado de 12 dimensões envolvendo funções transcendentais.
• Sistemas Híbridos: O framework gerou cerceamentos rigorosos para um sistema híbrido de bola saltitante (bouncing ball), projetando corretamente os flowpipes no plano $(x, t)$ enquanto distingue entre modos ativos (cima/baixo).
• Sistemas Estocásticos: O TERA computou um cerceamento $\delta$-PRS ($\delta = 0.001$) para um modelo de mola estocástica sobre $t \in [0, 20]$. O cerceamento resultante mostrou conter 2000 trajetórias de amostra de Monte Carlo de Euler-Maruyama.

Significância e Perspectivas Futuras
O artigo posiciona o TERA como um passo fundamental em direção a uma infraestrutura robusta, de código aberto e nativa de Python para análise de alcançabilidade rigorosa. Sua significância reside na democratização do acesso a métodos de TM de alta ordem para uma ampla classe de sistemas, incluindo aqueles com perturbações estocásticas. Os autores afirmam que o trabalho contínuo está focado em estender as capacidades para sistemas híbridos estocásticos. O objetivo de longo prazo é aplicar esta infraestrutura para classes de sistemas ainda mais amplas, como aquelas controladas por redes neurais artificiais. Os autores mantêm um tom modesto, observando que, embora a implementação atual lide com benchmarks difíceis, o framework foi projetado para evoluir para suportar classes de sistemas mais complexas.