Show simple item record

dc.contributor.authorDeCastro, Jonathan Anthony
dc.identifier.otherbibid: 9948875
dc.description.abstractWith 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.
dc.rightsAttribution 4.0 International*
dc.subjectComputer science
dc.subjectController synthesis
dc.subjectFormal logic
dc.subjectFormal verification
dc.subjectMission planning
dc.subjectNonlinear dynamical systems
dc.titleGuaranteeing Reactive Missions for Complex Robotic Systems
dc.typedissertation or thesis Engineering University of Philosophy D., Mechanical Engineering
dc.contributor.chairKress-Gazit, Hadas
dc.contributor.committeeMemberVladimirsky, Alexander
dc.contributor.committeeMemberKnepper, Ross A

Files in this item


This item appears in the following Collection(s)

Show simple item record

Except where otherwise noted, this item's license is described as Attribution 4.0 International