Explaining Unsynthesizability Of High-Level Robot Behaviors

Other Titles


As robots become increasingly capable and general-purpose, it is desirable for them to be easily controllable by a wide variety of users. The near future will likely see robots in homes and offices, performing everyday tasks such as fetching coffee and tidying rooms. There is therefore a growing need for non-expert users to be able to easily program robots performing complex high-level tasks. Such high-level tasks include behaviors comprising non-trivial sequences of actions, reacting to external events, and achieving repeated goals. Recent advances in the application of formal methods to robot control have enabled automated synthesis of correct-by-construction hybrid controllers for complex highlevel tasks. These approaches use a discrete abstraction of the robot workspace and a temporal logic specification of the environment assumptions and desired robot behavior, and yield controllers that are provably correct with respect to this abstraction and specification. However, there are many remaining challenges in ensuring that a user-defined specification yields a robot controller that achieves the desired high-level behavior. This dissertation addresses several causes of failure resulting from logical implications of the specification itself, as well as those arising because of inconsistencies between the discrete abstraction and the continuous execution domain. Work on three main challenges is described. The first is an algorithm for the analysis of logic specifications, which provides a high-level cause of failure for specifications that have no implementation, or unsynthesizable specifications. An interactive game is also introduced, allowing users to explore the cause of unsynthesizability. The second is the identification of a minimal explanation of failure: several techniques are presented to identify a core subset of the specification that causes unsynthesizability. The third problem addressed is the definition of an appropriate timing semantics for ion and execution of hybrid controllers synthesized from high-level specifications. Several controller-synthesis frameworks are compared, and their suitability to different problem domains discussed, based on their underlying assumptions and properties of the resulting continuous behaviors.

Journal / Series

Volume & Issue



Date Issued




Robotics; Formal Methods; Synthesis


Effective Date

Expiration Date




Union Local


Number of Workers

Committee Chair

Kress Gazit, Hadas

Committee Co-Chair

Committee Member

Selman, Bart
Easley, David Alan
Halpern, Joseph Yehuda

Degree Discipline

Computer Science

Degree Name

Ph. D., Computer Science

Degree Level

Doctor of Philosophy

Related Version

Related DOI

Related To

Related Part

Based on Related Item

Has Other Format(s)

Part of Related Item

Related To

Related Publication(s)

Link(s) to Related Publication(s)


Link(s) to Reference(s)

Previously Published As

Government Document




Other Identifiers


Rights URI


dissertation or thesis

Accessibility Feature

Accessibility Hazard

Accessibility Summary

Link(s) to Catalog Record