CS 6752 - [Formal Methods for Robotics]

(crosslisted) MAE 6770

Fall. Not offered: 2023-2024. Next offered: 2024-2025. 3 credits. Letter grades only.

Enrollment limited to: graduate students or permission of instructor.

H. Kress-Gazit.

How can we guarantee robots will never cause harm? How can we prove that complicated mechanical systems, controlled by computers and programmed by people, will always behave as expected under changing conditions and in a variety of uncertain environments? How do we formalize what such behaviors are? Guaranteeing safety, predictability and reliability of robots is crucial for the assimilation of such systems into society, be it at home or in the workplace. While every robotics researcher working with or on a robot is aware of safety issues, only recently the robotics community has begun looking at ways to either formally prove or grarantee by design different behavioral properties such as safety and correctness. This class will present recent results on the topic of formal methods for robotics and automation that combine and extend ideas from control theory, dynamical systems, automata theory, logic, model checking, synthesis, and hybrid systems.

Outcome 1: The student will be able to define specifications using different formalisms such as temporal logics and sets.

Outcome 2: The student will be able to explain different verification algorithms.

Outcome 3: The student will be able to explain the different approaches to control synthesis.

Outcome 4: The student will be able to present a state-of-the-art research paper in a way that conveys the main contribution of the paper.

Outcome 5: The student will be able to apply the tools learned in the class to their individually chosen project.