Synthesis for Robots: Guarantees and Feedback for Robot Behavior Journal Article uri icon



  • Robot control for tasks such as moving around obstacles or grasping objects has advanced significantly in the last few decades. However, controlling robots to perform complex tasks is still accomplished largely by highly trained programmers in a manual, time-consuming, and error-prone process that is typically validated only through extensive testing. Formal methods are mathematical techniques for reasoning about systems, their requirements, and their guarantees. Formal synthesis for robotics refers to frameworks for specifying tasks in a mathematically precise language and automatically transforming these specifications into correct-by-construction robot controllers or into a proof that the task cannot be done. Synthesis allows users to reason about the task specification rather than its implementation, reduces implementation error, and provides behavioral guarantees for the resulting controller. This article reviews the current state of formal synthesis for robotics and surveys the landscape of abstractions, specifications, and synthesis algorithms that enable it.

publication date

  • May 28, 2018

has restriction

  • bronze

Date in CU Experts

  • November 2, 2018 10:43 AM

Full Author List

  • Kress-Gazit H; Lahijanian M; Raman V

author count

  • 3

Other Profiles

International Standard Serial Number (ISSN)

  • 2573-5144

Electronic International Standard Serial Number (EISSN)

  • 2573-5144

Additional Document Info

start page

  • 211

end page

  • 236


  • 1


  • 1