Using SyGuS to Synthesize Reactive Motion Plans

TL;DR

This paper introduces a novel method for reactive robot motion planning by compiling the problem into SyGuS specifications, enabling the synthesis of a single reactive program capable of handling adversarial environments.

Contribution

First application of SyGuS formalism to robot motion planning, demonstrating its practicality for synthesizing reactive motion strategies in complex environments.

Findings

Successfully synthesized reactive motion plans using SyGuS

Handled environments with adversarial obstacles

Demonstrated practicality for bounded two-player reachability games

Abstract

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.