Guaranteeing Reactive Missions for Complex Robotic Systems

Other Titles


With the availability of robots capable of performing complex missions, formal approaches to controller synthesis are gaining increasing attention as a means for synthesizing controllers that guarantee, by construction, the execution of such missions. The approach frees users from having to hand-design such implementations and have utility for missions in which the system must maintain safety in dynamic, uncontrolled environments. For instance, a personal assistant might be entrusted to fetch a box from a location and then deliver it to the required location in the household, while avoiding collisions with closed doors, people, and static obstacles. In this work, three interrelated problems are solved, each addressing the overall problem of automatically synthesizing controllers with applicability to robots with complex, nonlinear dynamics. First, an off-line approach is introduced for synthesizing low-level controllers for nonlinear systems. The approach builds on sample-based motion planning and nonlinear system analysis techniques, and is capable of synthesizing a palette of controllers that certifies a task (mission instructions provided by a user via a formal specification). To address cases where a task cannot be guaranteed on a given physical platform, the second contribution is an automated approach to specification revisions using information contained in a discrete representation (i.e. abstraction) of the dynamical system. The user is provided with a concise yet expressive set of revisions as instructive feedback required to guarantee the specification. The final contribution is a novel synthesis approach that extends the revisions approach to enable a team of robots operating in workspaces shared with other agents (e.g., humans or cars). Whereas typical centralized controllers are combinatorially expensive to compute, our approach lessens this complexity while retaining correctness by leveraging a local motion planner and employing a high-level scheme that reasons about deadlock between two or more agents. Throughout this work, the various approaches are demonstrated through a variety of missions carried out both in simulation and on physical platforms in dynamic environments.

Journal / Series

Volume & Issue



Date Issued




Computer science; Controller synthesis; Formal logic; Formal verification; Mission planning; Nonlinear dynamical systems; Robotics


Effective Date

Expiration Date




Union Local


Number of Workers

Committee Chair

Kress-Gazit, Hadas

Committee Co-Chair

Committee Member

Vladimirsky, Alexander
Knepper, Ross A

Degree Discipline

Mechanical Engineering

Degree Name

Ph. D., Mechanical Engineering

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


Attribution 4.0 International


dissertation or thesis

Accessibility Feature

Accessibility Hazard

Accessibility Summary

Link(s) to Catalog Record