# Physically-Feasible Repair of Reactive, Linear Temporal Logic-based, High-Level Tasks

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 6 Jul 2022.

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

- [Plug in the Safety Chip: Enforcing Constraints for LLM-driven Robot Agents](https://mlsanity.com/paper/2309.09919/) (2023)
- [SPINE: Online Semantic Planning for Missions with Incomplete Natural Language Specifications in Unstructured Environments](https://mlsanity.com/paper/2410.03035/) (2024)
- [Traffic-Rule-Compliant Trajectory Repair via Satisfiability Modulo Theories and Reachability Analysis](https://mlsanity.com/paper/2412.15837/) (2024)
- [Learning to Bridge the Gap: Efficient Novelty Recovery with Planning and Reinforcement Learning](https://mlsanity.com/paper/2409.19226/) (2024)
- [Follow the STARs: Dynamic ω-Regular Shielding of Learned Policies](https://mlsanity.com/paper/2505.14689/) (2025)
- [INPROVF: Leveraging Large Language Models to Repair High-level Robot Controllers from Assumption Violations](https://mlsanity.com/paper/2503.13660/) (2025)

## Abstract (arXiv)

A typical approach to creating complex robot behaviors is to compose atomic controllers, or skills, such that the resulting behavior satisfies a high-level task; however, when a task cannot be accomplished with a given set of skills, it is difficult to know how to modify the skills to make the task possible. We present a method for combining symbolic repair with physical feasibility-checking and implementation to automatically modify existing skills such that the robot can execute a previously infeasible task. We encode robot skills in Linear Temporal Logic (LTL) formulas that capture both safety constraints and goals for reactive tasks. Furthermore, our encoding captures the full skill execution, as opposed to prior work where only the state of the world before and after the skill is executed are considered. Our repair algorithm suggests symbolic modifications, then attempts to physically implement the suggestions by modifying the original skills subject to LTL constraints derived from the symbolic repair. If skills are not physically possible, we automatically provide additional constraints for the symbolic repair. We demonstrate our approach with a Baxter and a Clearpath Jackal.