Value Functions for Temporal Logic: Optimal Policies and Safety Filters

Resumo Técnico: Funções de Valor para Lógica Temporal: Políticas Ótimas e Filtros de Segurança

Enunciado do Problema
Embora as equações de Bellman para problemas básicos de alcance, evitamento e alcance-evitamento sejam bem estabelecidas, a relação entre otimalidade de valor e otimalidade de política torna-se sutil em cenários de horizonte infinito sem desconto, particularmente para especificações complexas de Lógica Temporal (LT). Surge uma patologia crítica onde maximizar gananciosamente a função Q pode produzir políticas que adiam indefinidamente a conclusão da tarefa para problemas de alcance-evitamento (equivalentes a especificações Until), mesmo quando a própria função de valor é ótima. Isso ocorre porque a sequência de ações ótima para trajetórias infinitas é fundamentalmente não-Markoviana; a entrada ótima pode precisar "alternar" de maximizar o valor atual para um valor constituinte em um grafo de decomposição para satisfazer as especificações remanescentes de horizonte infinito. Métodos existentes, como a augmentação de estado para problemas de dupla objetivo, lutam para generalizar-se a fórmulas complexas envolvendo especificações aninhadas de Until, Globally e Globally-Until. Além disso, há uma necessidade de filtros de segurança que garantam a satisfação de especificações complexas de LT, indo além de tarefas simples de evitamento ou alcance-evitamento.

Metodologia
Os autores propõem um framework que generaliza funções de valor e Q para históricos de estado para lidar com a natureza não-Markoviana do problema. A metodologia baseia-se na decomposição algébrica da função de valor para LT em um grafo de funções de valor constituintes.

1. Funções de Valor Não-Markovianas: O artigo define funções de valor ótimas $V^*$ e funções Q sobre históricos de estado $x_{0:t}$ em vez de apenas estados atuais. Isso permite que a política leve em conta o histórico necessário para satisfazer as restrições temporais.
2. Sistemas com Augmentação Temporal e Tempos de Testemunha: Para abordar a questão do adiamento em especificações Until ($U$), os autores introduzem um sistema com augmentação temporal e um temporizador. Eles definem um "tempo de testemunha ótimo" $\sigma^*$, que é o tempo mais cedo em que uma trajetória atinge a pontuação ótima de robustez. Isso permite a construção de políticas que alternam de uma estratégia gananciosa de horizonte finito (maximizando a função Q dentro do tempo de testemunha) para uma política de sufixo que satisfaz a sub-fórmula remanescente.
3. Construção Compositiva de Políticas: O artigo constrói políticas ótimas para um fragmento específico de fórmulas de LT (Definição 3), que inclui:
   • Fórmulas proposicionais.
   • Operadores Until ($p U \phi$), Next ($X\phi$) e Globally ($Gp$).
   • Globally-Until ($G(\bigvee p_i U r_i)$), que codifica critérios de aceitação de Büchi.
   • Disjunções e conjunções proposicionais.
     A construção assume a existência de políticas ótimas para sub-fórmulas (Hipótese 2) e combina-as recursivamente. Para Globally-Until, a política visita iterativamente cada componente Until em sequência para garantir visitas infinitas aos conjuntos de estado requeridos.
4. Filtragem de Segurança: Os autores demonstram que a função Q pode servir como um filtro de segurança. Eles definem um conjunto de falha onde a especificação não pode ser satisfeita com robustez não-negativa. Um esquema de intervenção menos restritivo é proposto: se a ação de uma política nominal resultar em um valor Q não-negativo (indicando satisfatibilidade futura), ela é permitida; caso contrário, o sistema alterna para a ação que maximiza a função Q. Sob suposições específicas (por exemplo, ausência de operadores Until ilimitados), este filtro garante a satisfação da especificação.

Principais Contribuições

1. Generalização das Funções de Valor: O artigo generaliza a função de valor ótima e a função Q para históricos de estado (Definição 1) e define otimalidade sobre históricos (Definição 2), abordando a natureza não-Markoviana dos problemas de LT de horizonte infinito.
2. Políticas Ótimas Compositivas: Para uma ampla classe de fórmulas de LT (Definição 3), os autores constroem políticas ótimas compositivas para a métrica de robustez associada (Teoremas 1–8). Isso inclui o tratamento da patologia de adiamento em especificações Until e Globally-Until.
3. Filtros de Segurança Menos Restritivos: O trabalho mostra que a função Q sobre históricos (potencialmente sub-ótimos) produz um filtro de segurança menos restritivo para uma política nominal (Teoremas 9, 10). Este filtro garante a satisfação da especificação enquanto respeita o caminho anterior da política nominal, desde que a fórmula atenda a certas restrições estruturais.

Resultados e Demonstrações
O artigo valida o framework proposto através de provas teóricas e duas demonstrações de hardware/software:

• GridWorld de Dois Agentes: Os autores resolvem um problema conjunto de estado-ação de 4 dimensões com uma especificação complexa envolvendo restrições de alcance com limite de tempo, segurança e vivacidade. Eles demonstram que a política ótima derivada ($\pi_{spec}$) guia com sucesso o sistema para satisfazer a especificação. Além disso, quando usada como filtro para políticas nominais de "café" e "chá" (que individualmente falham em satisfazer a especificação conjunta), o filtro garante que o sistema conjunto satisfaça a tarefa complexa, ao passo que um filtro padrão "apenas segurança" leva a um impasse e falha.
• Drone de Agente Único: Usando um drone Crazyflie, os autores demonstram a política em uma tarefa de navegação com obstáculos. O filtro de LT proposto guia com sucesso o drone para um local de trabalho enquanto satisfaz restrições temporais complexas (por exemplo, looping através de zonas específicas, evitando paredes). Em contraste, uma política nominal não filtrada ou um filtro baseado apenas em restrições de segurança resulta no drone ficando preso ou colidindo.

Significado
O artigo afirma oferecer uma abordagem prática para gerar políticas ótimas para o valor de uma ampla classe de fórmulas de LT, estendendo resultados recentes de decomposição. Seu significado principal reside em resolver a patologia onde a maximização gananciosa de Q falha para tarefas de horizonte infinito e em fornecer um mecanismo para sintetizar filtros de segurança que garantam a satisfação de tarefas complexas, não apenas a segurança. Ao expandir o escopo de fórmulas solucionáveis para incluir especificações aninhadas de Until e Globally-Until, o trabalho preenche a lacuna entre a alcançabilidade de Hamilton-Jacobi e o Aprendizado por Reforço para tarefas temporais complexas e críticas para a segurança.