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.

翻译：虽然用于基本到达、避免及到达-避免问题的贝尔曼方程已被充分研究，但在未折扣无限时域设定下，值最优性与策略最优性之间的关系变得微妙，尤其对于更复杂的任务而言。对于到达-避免问题（等价于"直至"规范），即使值函数达到最优，贪婪最大化Q函数产生的策略仍可能无限期推迟任务完成。基于近期将时间逻辑值函数分解为若干组成值函数图结构的研究成果，我们构建了依赖状态历史的非马尔可夫策略，该策略能避免此类病态行为，并证明了此类策略对嵌套"直至"、"全局"及"全局-直至"规范的定量鲁棒性得分具有最优性。我们进一步展示了Q函数如何为复杂时间逻辑规范充当安全过滤器，将先前成果从简单的避免或到达-避免任务扩展至更广泛场景。