Robotics Engineering Colloquium Series: Dr. Kevin Leahy | Multi-Robot Formal Synthesis and Reinforcement Learning
Robotics Engineering Colloquium Series
Kevin Leahy, MIT Lincoln Laboratory
Multi-Robot Formal Synthesis and Reinforcement Learning
Friday, March 17th, 2023
1:30 PM - 2:30 PM
Unity Hall | Room 500
Abstract: Robotics and autonomous systems continue to have an ever-larger impact on the world around us. As robotic technology advances, it will bring great change to our world. It is critical that we ensure safe, reliable operation of these systems, without compromising performance. Formal methods is one approach for specifying goals and safety constraints for autonomous systems, with strong guarantees that a robotic system will meet those goals.
In this talk, I will present recent results in formal synthesis for robotics. First, I will review recent advances in formal synthesis for multi-agent planning and control. Scalability of the synthesis process is critical for large multi-agent systems, and the presented method reasons about complex specifications in order to decompose the specification into smaller specifications that can be assigned to individual agents or sub-teams of agents. This is accomplished using an abstract rewriting system to transform a formula in Signal Temporal Logic (STL) into a set of disjoint formulae whose satisfaction entails satisfaction of the original STL formula. Next, I will present methods for scaling formal synthesis when a model of the system is unavailable. Using model-free reinforcement learning, we design a method for training policies on individual tasks. The process is designed to allow both Boolean and temporal composition of those tasks. This process allows training for a small set of tasks to enable an exponential set of realizable behaviors, with guarantees on the execution of those behaviors
Bio: Dr. Kevin Leahy is a technical staff member in the Artificial Intelligence (AI) Technology Group at MIT Lincoln Laboratory. His current work involves AI for autonomous systems, with an emphasis on formal methods and multi-agent systems. His previous work at MIT Lincoln Laboratory focused on a variety of domains, including learning decentralized control strategies for multi-agent systems, researching collision avoidance in aviation, and planning for heterogeneous teams from high-level specifications.
Dr. Leahy received his BA degree in economics and MS and PhD degrees in mechanical engineering from Boston University. He currently serves as Junior Co-chair on the IEEE Technical Committee for Verification of Autonomous Systems.