Skip to content
AI News HubLIVE
Original source2 min read

Value Functions for Temporal Logic: Optimal Policies and Safety Filters

Summary

This research reveals that greedy maximization of the Q-function in undiscounted infinite-horizon settings can produce policies that indefinitely defer task completion. By decomposing the temporal logic value function into a graph of constituent value functions, the authors construct non-Markovian policies based on state history, proving their optimality for nested Until, Globally, and Globally-Until specifications, and extend the Q-function as a safety filter for complex TL specifications.

SourcearXiv RoboticsAuthor: Oswin So, William Sharpless, Sylvia Herbert, Chuchu Fan
Value Functions for Temporal Logic: Optimal Policies and Safety Filters
Report an error

The correction channel is not available yet. You can copy the article reference below for later.

Correction instructions
Read article

[2605.01051] Value Functions for Temporal Logic: Optimal Policies and Safety Filters

Skip to main content

Learn about arXiv becoming an independent nonprofit.

We gratefully acknowledge support from the Simons Foundation, member institutions, and all contributors. Donate

> cs > arXiv:2605.01051

Help | Advanced Search

All fields Title Author Abstract Comments Journal reference ACM classification MSC classification Report number arXiv identifier DOI ORCID arXiv author ID Help pages Full text

Search

GO

quick links

Login

Help Pages

About

-->

Computer Science > Robotics

arXiv:2605.01051 (cs)

[Submitted on 1 May 2026]

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

Authors:Oswin So, William Sharpless, Sylvia Herbert, Chuchu Fan

View a PDF of the paper titled Value Functions for Temporal Logic: Optimal Policies and Safety Filters, by Oswin So and 3 other authors

View PDF HTML (experimental)

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.

Subjects:

Robotics (cs.RO); Artificial Intelligence (cs.AI); Machine Learning (cs.LG); Logic in Computer Science (cs.LO); Optimization and Control (math.OC)

Cite as: arXiv:2605.01051 [cs.RO]

(or arXiv:2605.01051v1 [cs.RO] for this version)

https://doi.org/10.48550/arXiv.2605.01051

Focus to learn more

arXiv-issued DOI via DataCite (pending registration)

Submission history

From: Oswin So [view email] [v1] Fri, 1 May 2026 19:30:03 UTC (4,591 KB)

Full-text links:

Access Paper:

View a PDF of the paper titled Value Functions for Temporal Logic: Optimal Policies and Safety Filters, by Oswin So and 3 other authors

View PDF

HTML (experimental)

TeX Source

view license

Current browse context:

cs.RO

new | recent | 2026-05

Change to browse by:

cs cs.AI cs.LG cs.LO math math.OC

References & Citations

NASA ADS

Google Scholar

Semantic Scholar

export BibTeX citation Loading...

BibTeX formatted citation

×

loading...

Data provided by:

Bookmark

Bibliographic Tools

Bibliographic and Citation Tools

Bibliographic Explorer Toggle

Bibliographic Explorer (What is the Explorer?)

Connected Papers Toggle

Connected Papers (What is Connected Papers?)

Litmaps Toggle

Litmaps (What is Litmaps?)

scite.ai Toggle

scite Smart Citations (What are Smart Citations?)

Code, Data, Media

Code, Data and Media Associated with this Article

alphaXiv Toggle

alphaXiv (What is alphaXiv?)

Links to Code Toggle

CatalyzeX Code Finder for Papers (What is CatalyzeX?)

DagsHub Toggle

DagsHub (What is DagsHub?)

GotitPub Toggle

Gotit.pub (What is GotitPub?)

Huggingface Toggle

Hugging Face (What is Huggingface?)

ScienceCast Toggle

ScienceCast (What is ScienceCast?)

Demos

Demos

Replicate Toggle

Replicate (What is Replicate?)

Spaces Toggle

Hugging Face Spaces (What is Spaces?)

Spaces Toggle

TXYZ.AI (What is TXYZ.AI?)

Related Papers

Recommenders and Search Tools

Link to Influence Flower

Influence Flower (What are Influence Flowers?)

Core recommender toggle

CORE Recommender (What is CORE?)

Author

Venue

Institution

Topic

About arXivLabs

arXivLabs: experimental projects with community collaborators

arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.

Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.

Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.

Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?)

About

Help

contact arXivClick here to contact arXiv Contact

subscribe to arXiv mailingsClick here to subscribe Subscribe

Copyright

Privacy Policy

Web Accessibility Assistance

arXiv Operational Status

Key points and analysis

Article intelligence

EngineersAdvanced

Key points

  • Greedy Q-function can lead to policies that indefinitely defer task completion in infinite-horizon tasks
  • Non-Markovian policies based on state history avoid this pathology
  • Optimality is proven for nested temporal logic specifications
  • Q-function serves as a safety filter for complex temporal logic tasks

Highlights and analysis are generated automatically and may contain errors. Check the original source.