# Value Functions for Temporal Logic: Optimal Policies and Safety Filters

arXiv: https://arxiv.org/abs/2605.01051 · HTML: https://mlsanity.com/paper/2605.01051/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 9 of its 23 references that are in the map.
- First posted on arXiv 1 May 2026.

## Builds on (most cited first, 9 of 9)

- [Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances](https://mlsanity.com/paper/1709.07523/) (2017)
- [The Safety Filter: A Unified View of Safety-Critical Control in Autonomous Systems](https://mlsanity.com/paper/2309.05837/) (2023)
- [Safety and Liveness Guarantees through Reach-Avoid Reinforcement Learning](https://mlsanity.com/paper/2112.12288/) (2021)
- [Reach-Avoid Problems with Time-Varying Dynamics, Targets and Constraints](https://mlsanity.com/paper/1410.6445/) (2014)
- [Solving Minimum-Cost Reach Avoid using Reinforcement Learning](https://mlsanity.com/paper/2410.22600/) (2024)
- [Learning Stabilization Control from Observations by Learning Lyapunov-like Proxy Models](https://mlsanity.com/paper/2303.02215/) (2023)
- [Bellman Value Decomposition for Task Logic in Safe Optimal Control](https://mlsanity.com/paper/2602.19532/) (2026)
- [Dual-Objective Reinforcement Learning with Novel Hamilton-Jacobi-Bellman Formulations](https://mlsanity.com/paper/2506.16016/) (2025)
- [Solving Reach- and Stabilize-Avoid Problems Using Discounted Reachability](https://mlsanity.com/paper/2505.09067/) (2025)

## Built on by (most cited first, 1 of 1)

- [CrossSafe: Towards Cross-Embodiment Latent Safety Filters](https://mlsanity.com/paper/2609.28984/) (2026)

## Abstract (arXiv)

While Bellman equations for basic reach, avoid, and reach-avoid problems are well studied, the relationship between value optimality and policy optimality becomes subtle in the undiscounted infinite-horizon setting, particularly for more complicated tasks. Greedily maximizing the Q-function can produce policies that indefinitely defer task completion for reach-avoid problems, or equivalently, Until specifications, even when the value function is optimal. Building upon recent results decomposing the value function for temporal logic (TL) into a graph of constituent value functions, we construct non-Markovian policies based on state history that avoid this pathology and prove their optimality with respect to the quantitative robustness score for nested Until, Globally, and Globally-Until specifications. We further show how the Q function can serve as a safety filter for complex TL specifications, extending prior results beyond simple avoid or reach-avoid tasks.