On the Computation of Backward Reachable Sets for Max-Plus Linear Systems with Disturbances

Resumo Técnico: Cálculo de Conjuntos de Alcançabilidade Reversa para Sistemas Lineares Max-Plus com Perturbações

1. Problema Investigado

O artigo aborda o problema de alcançabilidade reversa de um passo (one-step backward reachability) para Sistemas Lineares Max-Plus (MPLS) sujeitos a perturbações aditivas.

• Contexto: Sistemas MPLS são amplamente utilizados para modelar sistemas de eventos discretos com sincronização e atrasos (ex: manufatura, transporte). No entanto, na prática, esses sistemas enfrentam incertezas devido a erros de modelagem, variações de parâmetros ou perturbações externas.
• Objetivo: Dado um conjunto de estados alvo (conjunto de segurança) $E$, o objetivo é computar o conjunto de estados iniciais a partir dos quais existe uma entrada de controle admissível tal que, para todas as perturbações admissíveis, o estado sucessor permaneça dentro do conjunto alvo $E$.
• Desafio: A presença de perturbações introduz uma quantificação universal sobre o conjunto de incerteza, tornando o problema significativamente mais complexo do que o caso sem perturbações. Métodos existentes baseados em Matrizes de Limites de Diferença (DBMs) podem tornar-se computacionalmente proibitivos à medida que a dimensão do sistema e a estrutura da incerteza crescem.

2. Metodologia e Abordagem

Os autores propõem uma nova estrutura computacional baseada na teoria de poliedros tropicais (tropical polyhedra) e na convexidade tropical.

• Representação das Incertezas: Ao contrário de abordagens probabilísticas ou de intervalos simples, o trabalho modela o conjunto de controle ($U$), o conjunto de perturbação ($W$) e o conjunto alvo ($E$) como poliedros tropicais. Isso oferece uma representação geométrica flexível e expressiva dentro da álgebra max-plus.
• Decomposição do Operador: O operador de alcançabilidade reversa $\Upsilon(E)$ é decomposto em três operadores elementares:
  1. Operador Inverso ($A^{-1}$): Relacionado à dinâmica autônoma do sistema.
  2. Operador Inverso Existencial ($\gamma_U$): Relacionado à existência de uma entrada de controle admissível.
  3. Operador Inverso Universal ($\phi_W$): Relacionado à quantificação universal sobre as perturbações (o desafio central).
• Preservação da Estrutura: O núcleo da metodologia é provar que a aplicação sequencial desses operadores sobre um poliedro tropical resulta, ainda, em um poliedro tropical. Isso permite que todo o cálculo seja realizado dentro do mesmo framework algébrico-geométrico.

Detalhes dos Algoritmos:

• Para $A^{-1}$ e $\gamma_U$: São desenvolvidos procedimentos para calcular a imagem inversa e a projeção existencial, mostrando que a estrutura de poliedro tropical é preservada e fornecendo métodos para determinar os vetores geradores do novo conjunto.
• Para $\phi_W$ (O Desafio Principal):
  • O conjunto de perturbação $W$ é decomposto na soma max-plus de um cone tropical (cone de recessão) e um poliedro tropical limitado.
  • O problema é simplificado verificando condições de não-vazio baseadas no cone de recessão.
  • O cálculo para a parte limitada é reformulado como uma interseção de pseudo-semiespaços.
  • Um algoritmo indutivo é proposto para calcular o conjunto gerador da interseção de múltiplos pseudo-semiespaços, utilizando um teorema análogo ao de Minkowski-Carathéodory na álgebra tropical.
  • Uma etapa de filtragem de pontos extremos é sugerida para reduzir a complexidade computacional, removendo geradores redundantes a cada iteração.

3. Contribuições Principais

1. Novo Framework Geométrico: Introdução do uso de poliedros tropicais para representar conjuntos de incerteza e estados em sistemas MPLS, superando as limitações das representações baseadas em intervalos.
2. Prova de Fechamento Estrutural: Demonstração teórica de que os operadores de alcançabilidade reversa (especialmente aquele com quantificação universal) preservam a estrutura de poliedro tropical. Isso garante que o conjunto de estados alcançáveis reversamente possa ser representado e computado de forma finita e exata.
3. Algoritmos Construtivos: Desenvolvimento de procedimentos algorítmicos explícitos para calcular os vetores geradores (representação interna ou V-form) dos conjuntos resultantes, incluindo a manipulação de pseudo-semiespaços e a determinação de parâmetros de interseção ($\rho$).
4. Análise de Complexidade e Filtragem: Proposta de técnicas para otimizar o cálculo, como a filtragem de pontos extremos, para mitigar o crescimento explosivo do número de geradores.

4. Resultados e Validação

• Exemplos Ilustrativos: O artigo inclui exemplos numéricos detalhados (Exemplos 1, 2 e 3) que demonstram a aplicação passo a passo dos algoritmos, incluindo a verificação de pertencimento a pseudo-semiespaços e o cálculo de vetores geradores.
• Estudo de Caso (Seção VII): Um estudo de caso completo é apresentado para um sistema MPLS de 2 estados com perturbações e controles definidos por poliedros tropicais.
  • O processo calcula sucessivamente $\phi_W(S)$, depois $\gamma_U(\phi_W(S))$ e finalmente $A^{-1}(\dots)$.
  • O resultado final é um conjunto de estados seguros representado como um poliedro tropical (convexa de pontos específicos), validando a viabilidade prática do método.
  • Figuras geométricas (Fig. 1 e Fig. 2) ilustram visualmente a relação entre o conjunto alvo, a perturbação e o conjunto de alcançabilidade reversa.

5. Significado e Impacto

Este trabalho oferece uma ferramenta poderosa para a análise de segurança e síntese de controladores em sistemas de eventos discretos sujeitos a incertezas determinísticas.

• Segurança Garantida: Ao fornecer o conjunto exato de estados iniciais seguros, permite a síntese de controladores que garantem a invariância do sistema dentro de limites de segurança, independentemente das perturbações admissíveis.
• Eficiência Computacional: A abordagem baseada em poliedros tropicais promete ser mais eficiente do que métodos baseados em DBMs para certas classes de problemas de alta dimensão, mantendo uma representação geométrica compacta.
• Perspectiva Futura: O trabalho abre caminho para futuras pesquisas focadas na melhoria da eficiência computacional (talvez com perda controlada de precisão) e na extensão para incertezas nos próprios parâmetros do sistema.

Em suma, o artigo estabelece uma ponte sólida entre a teoria de convexidade tropical e a análise de sistemas de controle híbrido/discreto, oferecendo métodos algébricos rigorosos para problemas de verificação formal em ambientes incertos.