Value Functions for Temporal Logic: Optimal Policies and Safety Filters

Resumen Técnico: Funciones de Valor para Lógica Temporal: Políticas Óptimas y Filtros de Seguridad

Enunciado del Problema
Mientras que las ecuaciones de Bellman para problemas básicos de alcance, evitación y alcance-evitación están bien establecidas, la relación entre optimalidad de valor y optimalidad de política se vuelve sutil en configuraciones de horizonte infinito sin descuento, particularmente para especificaciones complejas de Lógica Temporal (LT). Surge una patología crítica donde maximizar codiciosamente la función Q puede producir políticas que posponen indefinidamente la finalización de la tarea para problemas de alcance-evitación (equivalentes a especificaciones Until), incluso cuando la función de valor en sí misma es óptima. Esto ocurre porque la secuencia de acciones óptima para trayectorias infinitas es fundamentalmente no markoviana; la entrada óptima puede necesitar "cambiar" de maximizar el valor actual a un valor constituyente en un grafo de descomposición para satisfacer las especificaciones restantes de horizonte infinito. Los métodos existentes, como la ampliación de estados para problemas de doble objetivo, luchan por generalizarse a fórmulas complejas que involucran especificaciones anidadas de Until, Globally y Globally-Until. Además, existe una necesidad de filtros de seguridad que garanticen la satisfacción de especificaciones complejas de LT, yendo más allá de tareas simples de evitación o alcance-evitación.

Metodología
Los autores proponen un marco que generaliza las funciones de valor y Q a historiales de estados para manejar la naturaleza no markoviana del problema. La metodología se basa en la descomposición algebraica de la función de valor para LT en un grafo de funciones de valor constituyentes.

1. Funciones de Valor No Markovianas: El artículo define funciones de valor óptimas $V^*$ y funciones Q sobre historiales de estados $x_{0:t}$ en lugar de solo estados actuales. Esto permite que la política tenga en cuenta el historial requerido para satisfacer las restricciones temporales.
2. Sistemas Ampliados en el Tiempo y Tiempos de Testigo: Para abordar el problema de la postergación en especificaciones Until ($U$), los autores introducen un sistema ampliado en el tiempo con un temporizador. Definen un "tiempo de testigo óptimo" $\sigma^*$, que es el tiempo más temprano en que una trayectoria alcanza la puntuación de robustez óptima. Esto permite la construcción de políticas que cambian de una estrategia codiciosa de horizonte finito (maximizando la función Q dentro del tiempo de testigo) a una política de sufijo que satisface la subfórmula restante.
3. Construcción Composicional de Políticas: El artículo construye políticas óptimas para un fragmento específico de fórmulas de LT (Definición 3), que incluye:
   • Fórmulas proposicionales.
   • Operadores Until ($p U \phi$), Next ($X\phi$) y Globally ($Gp$).
   • Globally-Until ($G(\bigvee p_i U r_i)$), que codifica criterios de aceptación de Büchi.
   • Disyunciones y conjunciones proposicionales.
     La construcción asume la existencia de políticas óptimas para subfórmulas (Suposición 2) y las combina recursivamente. Para Globally-Until, la política visita iterativamente cada componente Until en secuencia para asegurar visitas infinitas a los conjuntos de estados requeridos.
4. Filtrado de Seguridad: Los autores demuestran que la función Q puede servir como un filtro de seguridad. Definen un conjunto de fallos donde la especificación no puede satisfacerse con robustez no negativa. Se propone un esquema de intervención menos restrictivo: si la acción de una política nominal produce un valor Q no negativo (indicando satisfacibilidad futura), se permite; de lo contrario, el sistema cambia a la acción que maximiza la función Q. Bajo suposiciones específicas (por ejemplo, ausencia de operadores Until no acotados), este filtro garantiza la satisfacción de la especificación.

Contribuciones Clave

1. Generalización de Funciones de Valor: El artículo generaliza la función de valor óptima y la función Q a historiales de estados (Definición 1) y define optimalidad sobre historiales (Definición 2), abordando la naturaleza no markoviana de los problemas de LT de horizonte infinito.
2. Políticas Óptimas Composicionales: Para una amplia clase de fórmulas de LT (Definición 3), los autores construyen políticas óptimas composicionales para la métrica de robustez asociada (Teoremas 1–8). Esto incluye el manejo de la patología de postergación en especificaciones Until y Globally-Until.
3. Filtros de Seguridad Menos Restrictivos: El trabajo muestra que la función Q sobre historiales (potencialmente subóptimos) produce un filtro de seguridad menos restrictivo para una política nominal (Teoremas 9, 10). Este filtro garantiza la satisfacción de la especificación mientras respeta la trayectoria previa de la política nominal, siempre que la fórmula cumpla ciertas restricciones estructurales.

Resultados y Demostraciones
El artículo valida el marco propuesto mediante pruebas teóricas y dos demostraciones de hardware/software:

• GridWorld de Dos Agentes: Los autores resuelven un problema conjunto de estado-acción de 4 dimensiones con una especificación compleja que involucra restricciones de alcance, seguridad y vivacidad acotadas en el tiempo. Demuestran que la política óptima derivada ($\pi_{spec}$) guía con éxito al sistema para satisfacer la especificación. Además, cuando se utiliza como filtro para políticas nominales de "café" y "té" (que individualmente no satisfacen la especificación conjunta), el filtro asegura que el sistema conjunto satisfaga la tarea compleja, mientras que un filtro estándar "solo de seguridad" conduce a un bloqueo y fallo.
• Drone de Agente Único: Utilizando un drone Crazyflie, los autores demuestran la política en una tarea de navegación con obstáculos. El filtro de LT propuesto guía con éxito al drone a un sitio de trabajo mientras satisface restricciones temporales complejas (por ejemplo, pasar en bucle por zonas específicas, evitar muros). Por el contrario, una política nominal sin filtrar o un filtro basado solo en restricciones de seguridad resulta en que el drone quede atrapado o choque.

Significado
El artículo afirma ofrecer un enfoque práctico para generar políticas óptimas para el valor de una amplia clase de fórmulas de LT mediante la extensión de resultados recientes de descomposición. Su principal significado radica en resolver la patología donde la maximización codiciosa de Q falla para tareas de horizonte infinito y en proporcionar un mecanismo para sintetizar filtros de seguridad que garanticen la satisfacción de tareas complejas, no solo la seguridad. Al extender el alcance de las fórmulas resolubles para incluir especificaciones anidadas de Until y Globally-Until, el trabajo cierra la brecha entre la alcanzabilidad de Hamilton-Jacobi y el Aprendizaje por Refuerzo para tareas temporales complejas y críticas para la seguridad.