PhD Dissertation
Explaining Unsynthesizability of High-Level Robot Behaviors
Abstract
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 high-level 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 abstraction 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.
[pdf]
