ARIA Systems group develops novel theoretical foundations and computational frameworks to enable reliable and intelligent autonomy. The main theme of our work is safety and soundness, and the emphasis is on safe autonomy through correct-by-construction algorithmic approaches. Our research builds on knowledge developed in control theory, formal methods, statistical reasoning, and machine learning & AI to address real-world challenges in robotics and safety-critical systems.

Current Projects

Verifiable Control Synthesis through Model-based Learning with Safety Guarantees

We are combining formal control synthesis and machine learning to tackle uncertainty in autonomous systems applications. By carefully considering the error in the learning process, we aim to develop novel methods for safe control that can adapt to changes in the system and environment.

Explainable Multi-Agent Planning

As we begin employing teams of robots to accomplish complex tasks, it becomes difficult for a human to verify that future paths do not result in collisions. Therefore, we are working on new multiagent planning approaches that minimize the effort it takes a human to verify the paths.

Expert-Informed Autonomous Science Planning for In-situ Observations and Discoveries

In this project, we are developing a framework to maximize science obtained by robotic landers in future space missions on the surface of distant bodies such as Europa. The key challenges we address is to reduce the dependency of human-in-the-loop operations and changes in the environment for limited-time missions by developing correct-by-construction algorithmic approaches that integrate formal method, game theory, and control theory.

INPASS: Intelligent Navigation, Planning, and Awareness for Swarm Systems

This project addresses the need to balance competing objectives for multi-agent autonomous systems in exploration of an environment. We aim to provide formal guarantees on performance and resource consumption objectives by using formal analysis techniques.

Safe driver assistance systems through cognitive modeling and reactive synthesis

This project studies the application of formal methods to the verification of a human driver model built using the cognitive architecture, and to the design of correct-by-construction Advanced Driver Assistance Systems (ADAS).

Mapping and motion planning for safe autonomous navigation

In real-world robotics, motion planning remains to be an open challenge. Not only robotic systems are required to move through unexplored environments, but also their maneuverability is constrained by their dynamics and often suffer from uncertainty.

Correct-by-Construction Controller Synthesis using Gaussian Process Transfer Learning

This project explores improvements to embedded control software for safety-critical cyber-physical systems with applications in autonomous transportation, traffic networks, power networks, and aerospace systems. These systems often have complex dynamics that are difficult to obtain in a closed-form and ensure their safety.

Enabling Long-term Marine Robotic Autonomy, from Learning Specifications to Autonomous Navigation and Interaction

In this project, we explore the challenges of developing smart and safe long-term autonomy for underwater vehicles.

Past Work

Resource-performance trade-off for mobile robot design
Specification revision with optimal satisfaction guarantees
Decision making and Planning in partially unknown environments
Planning for probabilistic robots with complex missions
Automatic control synthesis from high-level specifications
Verification and synthesis for stochastic hybrid systems