# CAREER: Structured Learning and Verification of Control Policies for Linear Temporal Logic Objectives

> **NSF 01003031DB NSF RESEARCH & RELATED ACTIVIT** · Rutgers University New Brunswick (NJ) · $599,549

## Abstract

The project investigates how to make intelligent robots more reliable, understandable, and safe when performing complex tasks over long periods of time. Modern learning-based systems can achieve impressive performance, but they often lack guarantees about correctness and safety, especially when tasks involve sequencing, repetition, and conditional behavior. The project addresses these challenges by combining robot learning with rigorous reasoning techniques. The project's novelties are a formulation that embeds temporal logic task constraints directly into the reinforcement learning objective to translate temporal progress into informative reward signals, a mechanism for automatically inferring temporal task specifications, and compositional methods for verifying long-horizon agent behaviors. The project's impacts are the development of trustworthy robotic systems capable of operating in uncertain environments, improved accessibility of formal methods for non-expert users, and new foundations for reliable AI/ML systems. The project will also benefit AI/ML tools and toolchains by introducing verification components that can be integrated into existing learning pipelines. In addition, the resulting algorithms and software provide reusable capabilities for specification inference and compositional verification in broader AI systems. The project will introduce formal methods into K–12 and undergraduate classrooms through the development of an interactive robot simulation tool that connects formal task specifications with robot behaviors, supporting hands-on coursework and mentoring activities that prepare a workforce trained in formal methods for building trustworthy systems.


The project develops a principled framework for synthesizing and verifying robot control policies for Linear Temporal Logic (LTL) objectives in continuous, stochastic environments. The framework leverages Limit-Deterministic Buchi Automata (LDBAs) as an abstract representation to guide both le

## Key facts

- **NSF award ID:** 2544018
- **Awardee organization:** Rutgers University New Brunswick (NJ)
- **SAM.gov UEI:** M1LVPE5GLSD9
- **PI:** He Zhu
- **Primary program:** 01003031DB NSF RESEARCH & RELATED ACTIVIT
- **All programs:** Artificial Intelligence (AI), CAREER-Faculty Erly Career Dev, SOFTWARE & HARDWARE FOUNDATION, Formal Methods and Verification
- **Estimated total:** $599,549
- **Funds obligated:** $395,821
- **Transaction type:** Continuing Grant
- **Period:** 05/01/2026 → 04/30/2031

## Primary source

NSF Award Search: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2544018

## Citation

> US National Science Foundation, Award 2544018, CAREER: Structured Learning and Verification of Control Policies for Linear Temporal Logic Objectives. Retrieved via AI Analytics 2026-07-04 from https://api.ai-analytics.org/grant/nsf/2544018. Licensed CC0.

---

*[NSF Awards dataset](/datasets/nsf-awards) · CC0 1.0*