Value Functions for Temporal Logic: Optimal Policies and Safety Filters

TL;DR

This paper explores the relationship between value functions and policies in temporal logic tasks, proposing non-Markovian policies that ensure optimality and safety in complex specifications.

Contribution

It introduces a method to construct history-dependent policies for temporal logic tasks that avoid suboptimal behaviors and serve as safety filters, extending prior results.

Findings

Constructed non-Markovian policies that are optimal for nested temporal logic specifications.

Proved the optimality of these policies with respect to robustness scores.

Demonstrated how Q functions can act as safety filters for complex temporal logic tasks.

Abstract

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.