Most of my work draws inspiration from practical applications, especially in autonomy, robotics, and transportation. As these systems become more complex, they cannot be built based on human intuition alone anymore. My research focuses on providing theoretical and computational foundations to enable systematic modeling, design, optimization, and analysis for such complex systems.

During my Ph.D., I led the Systems team and implemented the finite state machine logic that accounted for traffic rules and governed the overall functioning of the planner of Alice, Team Caltech’s entry in the 2007 DARPA Urban Challenge. The difficulties in the design and analysis of this finite state machine motivated my research on applying formal methods to control systems as part of the MURI project on Specification, Design and Verification of Distributed Embedded Systems. During my postdoc at SMART, I worked on building low-cost autonomous vehicles for mobility-on-demand systems, developing distributed algorithms for controlling traffic lights, and designing transportation pricing strategies to reduce traffic congestion.

I also spent 4+ years at a self-driving car company, nuTonomy, where I initially led the planning team and was a primary developer of the planning and decision-making module. Unlike in Alice, nuTonomy’s planning system does not rely on complex finite state machines. Instead, we applied formal methods to automatically build the decision-making logic such that it is provably correct by construction. While I was excited to see the core part of my research in real-world practices, I realized that there is a fundamental problem that has been mostly overlooked by the formal methods community and lies in the lack of precise specifications of these autonomous systems, i.e., in defining what constitutes their correct behaviors, taking into account various factors, including safety, regulatory requirements, comfort, culture, etc, that may be conflicting. My recent work focuses on addressing this gap and developing theory, methods, and tools to derive, analyze, and refine specifications for autonomous systems.

Sharing the World with Autonomous Systems: What Goes Wrong and How to Fix It (NSF)

Develop efficient algorithms for autonomous systems to characterize and actively identify the inconsistencies (e.g., in perception and decision-making) among the interacting agents and to influence the behaviors of the other agents to improve the safety of the overall system.

CAREER: Establishing Correctness of Learning-Enabled Autonomous Systems with Conflicting Requirements (NSF)

Develop specification formalisms, control synthesis algorithms, and quantitative verification frameworks for autonomous systems that include learning-based components, operate in uncertain environments, and are subject to conflicting requirements with partially established priorities.

Developing a Low Visibility Navigation System (Iowa DOT)

Develop and retrofit an existing snowplow with a suite of sensors and mapping systems along with a driver assistance interface that will guide the operator when visibility

Resource-Aware Hierarchical Runtime Verification for Mixed-Abstraction-Level Systems of Systems (NSF)

Develop runtime verification techniques that incorporate mixed-abstraction-level granularity in specifications and enable on-deadline mitigation triggering

Planning with Conflicting Specifications

Develop planning and decision-making algorithms with multiple, potentially conflicting objectives.

Formal Specifications of Autonomous Systems

Derive, analyze, and refine specifications from regulatory requirements and demonstrations.

Autonomy in Mobility-on-Demand Systems

Assess and demonstrate the role of autonomy in mobility-on-demand systems through modeling, algorithm development and experimental demonstration.

Video

Real-time Control and Learning for Sustainable Transportation

Mechanism design for dynamic pricing and real-time control of traffic signals based on control, communication, optimization and game theory

Video

Temporal Logic Planning (TuLiP) Toolbox

A Python-based software toolbox for the synthesis of embedded control software that is provably correct with respect to an expressive subset of linear temporal logic (LTL) specifications.

Code Slides

Consensus Approaches to the Assignment Problem

Design a consensus protocol to solve the assignment problem in a distributed manner.

Formal Methods for Design and Verification of Embedded Control Systems

Develop mathematical and computational frameworks to facilitate the design and analysis of embedded control systems such as autonomous vehicles.

Video

DARPA Urban Challenge 2007

A race of autonomous ground vehicles through an urban environment.

Video

Abstraction-Based Multi-Vehicle Command and Control

A path planning system for multi-vehicle domains.