On the Optimality of Uncertain MDP Abstractions

Título: Sobre a Optimalidade de Abstrações de MDPs Incertos (UMDPs)

Autores: Ibón Gracia e Morteza Lahijanian
Instituição: Universidade do Colorado, Boulder

---

1. Problema Investigado

O artigo aborda o desafio de síntese de controle formal para sistemas estocásticos não lineares complexos (como sistemas ciber-físicos de segurança crítica) sujeitos a especificações de lógica temporal (LTLf - Linear Temporal Logic over finite traces).

O problema central é a otimalidade assintótica das abordagens baseadas em abstração:

• Métodos existentes abstraem o sistema contínuo em um MDP Incerto (UMDP) para garantir limites de probabilidade de satisfação de especificações.
• No entanto, muitas dessas abordagens (especialmente as que usam IMDPs - Interval MDPs) não garantem que o refinamento da abstração (tornar a discretização mais fina) leve a limites de erro mais apertados ou à convergência para a probabilidade de satisfação ótima real.
• Em alguns casos, o refinamento pode até degradar os limites ou falhar em convergir, tornando impossível garantir um controlador $\epsilon$-ótimo em tempo finito.

O objetivo é identificar sob quais condições os métodos de abstração UMDP são assintoticamente ótimos (ou seja, o erro tende a zero à medida que a discretização fica infinitamente fina) e garantir a completude do algoritmo (terminação em tempo finito para qualquer margem de erro $\epsilon$).

2. Metodologia

Os autores propõem uma estrutura teórica e algorítmica baseada nos seguintes pilares:

A. Formulação do Sistema e Especificação

• Sistema: Modelado como um sistema estocástico de tempo discreto com dinâmicas não lineares gerais e perturbações i.i.d.
• Especificação: Fórmulas LTLf que definem comportamentos temporais (ex: "evitar zonas perigosas e eventualmente atingir um objetivo").
• Objetivo: Sintetizar um controlador que maximize a probabilidade de satisfação da especificação dentro de um horizonte de tempo $T$, com limites de erro garantidos.

B. Abstração e Refinamento Iterativo

O trabalho utiliza um framework de Abstração-Refinamento:

1. Abstração: O espaço de estado contínuo é particionado em regiões finitas, criando um UMDP.
2. Síntese: Um controlador é sintetizado no UMDP usando Programação Dinâmica Robusta (RDP) sobre o produto do UMDP com um Autômato Finito Determinístico (DFA) da especificação.
3. Verificação: Calculam-se limites inferior ($\underline{p}$) e superior ($\overline{p}$) para a probabilidade de satisfação.
4. Refinamento: Se a lacuna entre os limites ($\overline{p} - \underline{p}$) for maior que $\epsilon$, o particionamento é refinado e o processo repete.

C. Condição de "Ambiguidade Vanishing" (Ambiguidade Desvanecente)

A contribuição teórica central é a definição de uma condição suficiente para a optimalidade assintótica chamada ambiguidade vanishing.

• Diâmetro de Ambiguidade ($\phi$): Uma medida do tamanho do conjunto de distribuições de probabilidade possíveis (conjunto de ambiguidade) para cada par estado-ação no UMDP, medido pela distância de Wasserstein.
• Condição: O processo de abstração é assintoticamente ótimo se, e somente se, o diâmetro de ambiguidade tender a zero à medida que o tamanho da partição ($\eta$) tende a zero ($\lim_{\eta \to 0} \phi(\text{Abs}(S, \eta)) = 0$).

3. Principais Contribuições

1. Condição Suficiente de Optimalidade Assintótica:
   Os autores derivam e provam que a condição de "ambiguidade vanishing" garante que o algoritmo de refinamento converge para a solução ótima e que os limites de erro desaparecem. Isso resolve a questão fundamental de quando a refinamento melhora os resultados.

2. Análise Comparativa de Classes de UMDP:
   O artigo demonstra que diferentes métodos de abstração têm comportamentos distintos quanto à optimalidade:

   • SMDPs (Set-valued MDPs): Abstrações baseadas em conjuntos de estados alcançáveis (reach sets) satisfazem a condição de ambiguidade vanishing. Portanto, são assintoticamente ótimos.
   • IMDPs (Interval MDPs): Abstrações populares que usam intervalos de probabilidade para cada transição não satisfazem essa condição em geral. O artigo prova, via contraexemplo, que IMDPs podem falhar em convergir para a solução ótima, mantendo uma lacuna de erro não nula mesmo com refinamento infinito.

3. Algoritmo de Síntese $\epsilon$-Ótimo Completo:
   Propõem um algoritmo (Algoritmo 1) que, para qualquer procedimento de abstração que satisfaça a condição de ambiguidade vanishing, garante a síntese de um controlador $\epsilon$-ótimo em tempo finito para qualquer especificação LTLf.

4. Otimização de Particionamento:
   Introduzem uma variação da abstração SMDP que particiona apenas o conjunto de estados seguros ($X_{safe}$) e trata todo o conjunto inseguro como um único estado, reduzindo a complexidade computacional sem perder a optimalidade.

4. Resultados e Validação Empírica

Os resultados foram validados em dois estudos de caso:

• Caso 1: Regulação de Temperatura (1D):

  • Objetivo: Manter a temperatura em uma faixa segura e atingir um objetivo.
  • Resultado: O método baseado em SMDP convergiu rapidamente, reduzindo a lacuna de erro para menos de 2% em 8 iterações. O método baseado em IMDP não mostrou melhora significativa com o refinamento, mantendo limites de erro grandes (lacuna próxima de 1).

• Caso 2: Modelo de Carrinho Não Linear (2D):

  • Objetivo: Navegar em um ambiente com obstáculos, água e carpete, seguindo uma especificação LTLf complexa (ex: secar no tapete antes de carregar).
  • Resultado: Similar ao caso 1D. Os limites de probabilidade obtidos via SMDP tornaram-se mais apertados e precisos com o refinamento. Os limites via IMDP permaneceram "vagos" (próximos de [0, 1]) em grande parte do espaço de estados, indicando que o refinamento não resolveu a incerteza excessiva introduzida pela abstração.

5. Significado e Impacto

• Fundamentação Teórica: O trabalho estabelece as bases teóricas para a optimalidade assintótica em síntese de controle baseada em abstração, preenchendo uma lacuna crítica na literatura onde a convergência não era garantida para especificações temporais complexas.
• Guia Prático: Demonstra que o uso de IMDPs, embora comum e computacionalmente conveniente em alguns cenários, pode ser fundamentalmente inadequado para garantir soluções ótimas em sistemas não lineares gerais. Recomenda-se o uso de SMDPs ou métodos que garantam a condição de ambiguidade vanishing.
• Garantia de Desempenho: Oferece um método que não apenas fornece limites de segurança, mas garante que esses limites podem ser arbitrariamente apertados através do refinamento, permitindo a implantação confiável de sistemas de segurança crítica com garantias formais rigorosas.

Em resumo, o artigo prova que a qualidade da abstração (especificamente a forma como a incerteza é modelada) é mais importante do que apenas o tamanho da discretização, e identifica que abstrações baseadas em conjuntos (SMDP) são superiores às baseadas em intervalos (IMDP) para garantir a convergência para a solução ótima.