The Automata Lab focuses on developing the next generation of autonomous robotic technology, with an emphasis on formal methods, machine learning (ML), planning, and control. Our work strives to create intelligent mobile robots capable of independent decision-making backed by the strong guarantees provided by formal methods. We envision robots that can act on high-level input from a human operator, correctly and reliably, while interacting with objects, people, and other agents in real-world environments.
Our work falls under two primary thrusts:
- Applying tools from formal methods to real-world systems. This entails extending methods from automata- and optimization-based planning from specifications to include real-world uncertainties. Much prior work in planning from specifications makes strong assumptions on an agent’s ability to localize itself, or to identify labels in its environment. These assumptions are often too strong for real-world scenarios. For example, our work has covered planning in belief space from temporal logic specifications. We are currently investigating methods for estimation uncertainty from semantic SLAM and CNN-based localization into temporal logic planning.
- Applying formal methods to ML methods for planning and control. This work includes providing guarantees on ML-based control and estimation, especially in terms of safety guarantees. For example, while traditional approaches to planning and control have developed methods for accounting for well-understood noise and error models, e.g., Gaussian white noise, errors from ML systems are not as well-understood, and therefore new techniques must be developed to model and adapt to errors from ML systems.