Bernstein-based polynomial approach to study the stability of switched systems and formal verification using HOL Light

Resumo Técnico: Abordagem Polinomial Baseada em Bernstein para Estabilidade de Sistemas Comutados e Verificação Formal

Definição do Problema
Sistemas comutados, compostos por múltiplos subsistemas governados por um sinal de comutação, apresentam desafios significativos na análise de estabilidade. Métodos tradicionais frequentemente têm dificuldade em fornecer uma descrição matemática unificada do comportamento completo do sistema, particularmente quando o sinal de comutação é complexo (por exemplo, dependente do estado ou do tempo). Embora existam inúmeros métodos para analisar esses sistemas, há uma necessidade de uma formulação que possa transformar a lógica de comutação discreta em uma expressão polinomial contínua, facilitando assim a construção de funções de Lyapunov e permitindo a verificação formal rigorosa.

Metodologia
O artigo propõe uma estratégia para reformular sistemas comutados usando interpolação de Bernstein. A abordagem central envolve as seguintes etapas:

1. Reformulação Polinomial: O sinal de comutação $\sigma$, que dita a ativação dos subsistemas $f_i$, é aproximado usando polinômios de Bernstein. Ao expressar o sinal de comutação como uma combinação linear de funções de base de Bernstein, todo o sistema comutado (originalmente definido por equações diferenciais por partes) é transformado em uma única expressão polinomial unificada.

   • O sistema é inicialmente descrito como uma combinação convexa de subsistemas: $\dot{x} = \sum f_i(x)\sigma_i$, onde $\sum \sigma_i = 1$ e $\sigma_i \geq 0$.
   • O sinal de comutação $\sigma_i$ é substituído por sua aproximação de série de Bernstein $B_{i,m}^\sigma(\sigma(\nu), \nu)$, resultando em um "sistema B-comutado" descrito por uma única equação diferencial polinomial.

2. Tratamento de Tipos de Comutação: O método acomoda diferentes comportamentos de comutação:

   • Comutação dependente do estado: Modelada usando funções de sinal (por exemplo, $\sigma \equiv \text{sign}(\delta x_1 x_2)$), aproximada por polinômios de Bernstein de um grau $m$ específico.
   • Comutação dependente do tempo: Modelada usando funções de pulso para representar a ativação periódica.
   • Flexibilidade: O grau $m$ do polinômio de Bernstein pode ser ajustado para refinar a aproximação, ou regras de composição podem ser aplicadas para maior precisão, embora isso aumente a complexidade das expressões resultantes.

3. Verificação Formal: Uma vez que o sistema é representado como um polinômio, os autores propõem o uso do assistente de prova HOL Light para verificar formalmente as propriedades de estabilidade.

   • Uma função de Lyapunov candidata $V(x)$ é identificada para o sistema polinomial.
   • A tarefa de verificação é reduzida a provar a desigualdade $\dot{V}(x) < \epsilon$ (onde $\epsilon$ é uma constante positiva pequena) sobre um domínio $D$.
   • Isso é alcançado usando aritmética de intervalos com aproximações de Taylor, um método previamente validado no projeto Flyspeck. Isso permite a certificação rigorosa de que a derivada de Lyapunov é negativa (ou suficientemente próxima de zero) dentro dos limites especificados.

Principais Resultados
O artigo ilustra a abordagem proposta através de dois exemplos numéricos derivados da literatura existente, comparando a representação polinomial "B-comutada" contra o sistema comutado "padrão":

• Exemplo 1 (Sistema Estável): Um sistema comutado linear com dois subsistemas estáveis foi analisado. A aproximação de Bernstein conseguiu mimetizar o comportamento estabilizador do sistema padrão.
• Exemplo 2 (Sistema Instável): Um sistema comutado linear com subsistemas instáveis foi analisado. O método capturou corretamente o comportamento divergente, observando que, à medida que o produto do estado $x_1 x_2$ cresce além do intervalo $[0, 1]$, a série de Bernstein naturalmente diverge, refletindo a instabilidade do sistema.
• Verificação Formal: Um sistema linear estável básico foi utilizado para demonstrar o processo de verificação do HOL Light. Os autores geraram com sucesso um certificado de prova formal confirmando que a derivada de uma função de Lyapunov quadrática permaneceu abaixo de um limite ($\epsilon = 0,01$) dentro do intervalo $[0, 1]$.

Significância e Alegações
Os autores apresentam este trabalho como um estudo preliminar com as seguintes contribuições e limitações específicas:

• Unificação: A principal contribuição é a capacidade de "unificar" múltiplos subsistemas de comutação em uma única expressão polinomial via interpolação de Bernstein. Isso simplifica a busca por funções candidatas de Lyapunov.
• Certificação Formal: A abordagem preenche a lacuna entre a simulação numérica e a prova formal, permitindo que o assistente HOL Light verifique as propriedades de estabilidade das funções de Lyapunov derivadas.
• Escopo Modesto: O artigo afirma explicitamente que assume que as propriedades de estabilidade do sistema B-comutado são equivalentes às do sistema comutado padrão (pelo menos no que diz respeito à estabilidade de Lyapunov), mas não reivindica ter provado essa equivalência rigorosamente ainda.
• Trabalhos Futuros: Os autores identificam várias áreas para investigação futura, incluindo:
  • Provar a equivalência matemática completa entre as representações padrão e B-comutada em relação à estabilidade.
  • Estender o método para sistemas não lineares e não polinomiais.
  • Utilizar ferramentas de Soma de Quadrados (SOS) para calcular funções de Lyapunov "ótimas" em vez de apenas verificar candidatas identificadas.

Em conclusão, o artigo propõe um novo framework que utiliza polinômios de Bernstein para converter a análise de sistemas comutados em um problema polinomial, passível de ser resolvido via ferramentas de verificação formal, oferecendo um caminho potencial para a certificação rigorosa de estabilidade.