# Neurosymbolic Motion and Task Planning for Linear Temporal Logic Tasks

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

## Key facts

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

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

- [Conformal Temporal Logic Planning using Large Language Models](https://mlsanity.com/paper/2309.10092/) (2023)
- [Reward Machines for Deep RL in Noisy and Uncertain Environments](https://mlsanity.com/paper/2406.00120/) (2024)
- [Defining neurosymbolic AI](https://mlsanity.com/paper/2507.11127/) (2025)
- [BERN-NN: Tight Bound Propagation For Neural Networks Using Bernstein Polynomial Interval Arithmetic](https://mlsanity.com/paper/2211.14438/) (2022)
- [As You Wish: Mission Planning with Formal Verification using LLMs in Precision Agriculture](https://mlsanity.com/paper/2606.18519/) (2026)
- [Neuro-Symbolic Closed-Loop Control of Laser Powder Bed Fusion with an In-Loop Ontology](https://mlsanity.com/paper/2608.05773/) (2026)

## Abstract (arXiv)

This paper presents a neurosymbolic framework to solve motion planning problems for mobile robots involving temporal goals. The temporal goals are described using temporal logic formulas such as Linear Temporal Logic (LTL) to capture complex tasks. The proposed framework trains Neural Network (NN)-based planners that enjoy strong correctness guarantees when applying to unseen tasks, i.e., the exact task (including workspace, LTL formula, and dynamic constraints of a robot) is unknown during the training of NNs. Our approach to achieving theoretical guarantees and computational efficiency is based on two insights. First, we incorporate a symbolic model into the training of NNs such that the resulting NN-based planner inherits the interpretability and correctness guarantees of the symbolic model. Moreover, the symbolic model serves as a discrete "memory", which is necessary for satisfying temporal logic formulas. Second, we train a library of neural networks offline and combine a subset of the trained NNs into a single NN-based planner at runtime when a task is revealed. In particular, we develop a novel constrained NN training procedure, named formal NN training, to enforce that each neural network in the library represents a "symbol" in the symbolic model. As a result, our neurosymbolic framework enjoys the scalability and flexibility benefits of machine learning and inherits the provable guarantees from control-theoretic and formal-methods techniques. We demonstrate the effectiveness of our framework in both simulations and on an actual robotic vehicle, and show that our framework can generalize to unknown tasks where state-of-the-art meta-reinforcement learning techniques fail.