Robotics and Automation Society
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.
Many existing approaches for coordinating heterogeneous teams of robots either consider small numbers of agents, are application-specific, or do not adequately address common real-world requirements, e.g., strict deadlines or intertask dependencies. We introduce scalable and robust algorithms for task-based coordination from high-level specifications (ScRATCHeS) to coordinate such teams. We define a specification language, capability temporal logic, to describe rich, temporal properties involving tasks requiring the participation of multiple agents with multiple capabilities, e.g., sensors or end effectors. Arbitrary missions and team dynamics are jointly encoded as constraints in a mixed integer linear program, and solved efficiently using commercial off-the-shelf solvers. ScRATCHeS optionally allows optimization for maximal robustness to agent attrition at the penalty of increased computation time. We include an online replanning algorithm that adjusts the plan after an agent has dropped out. The flexible specification language, fast solution time, and optional robustness of ScRATCHeS provide a first step toward a multipurpose on-the-fly planning tool for tasking large teams of agents with multiple capabilities enacting missions with multiple tasks. We present randomized computational experiments to characterize scalability and hardware demonstrations to illustrate the applicability of our methods.