# Using SyGuS to Synthesize Reactive Motion Plans

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 23 Nov 2016.

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

- [Guiding Enumerative Program Synthesis with Large Language Models](https://mlsanity.com/paper/2403.03997/) (2024)
- [Reinforcement Learning and Data-Generation for Syntax-Guided Synthesis](https://mlsanity.com/paper/2307.09564/) (2023)
- [Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications](https://mlsanity.com/paper/2603.06710/) (2026)

## Abstract (arXiv)

We present an approach for synthesizing reactive robot motion plans, based on compilation to Syntax-Guided Synthesis (SyGuS) specifications. Our method reduces the motion planning problem to the problem of synthesizing a function that can choose the next robot action in response to the current state of the system. This technique offers reactivity not by generating new motion plans throughout deployment, but by synthesizing a single program that causes the robot to reach its target from any system state that is consistent with the system model. This approach allows our tool to handle environments with adversarial obstacles. This work represents the first use of the SyGuS formalism to solve robot motion planning problems. We investigate whether using SyGuS for a bounded two-player reachability game is practical at this point in time.