DeCastro, Jonathan Anthony2017-07-072017-07-072017-05-30DeCastro_cornellgrad_0058F_10192http://dissertations.umi.com/cornellgrad:10192bibid: 9948875https://hdl.handle.net/1813/51652With 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.en-USAttribution 4.0 InternationalComputer scienceController synthesisFormal logicFormal verificationMission planningNonlinear dynamical systemsRoboticsdissertation or thesishttps://doi.org/10.7298/X4PK0D9B