My research lies in the fields of robotics and automation, and focuses on developing controller software that can intelligently and reliably react to dynamic environments and unexpected events.

I am currently employed as an NRC Research Associate at the U.S. Naval Research Laboratory, where I am conducting research on the use of formally synthesized controllers as behavior-switching state machines for teams of robots that are providing support for disaster relief operations.  Additionally, I am investigating how Goal Reasoning techniques can enhance the teams’ ability to make intelligent decisions during execution.

My prior research, leading to my PhD, investigated the probabilistic modeling and analysis of formally synthesized controllers, when operating with erroneous sensors and actuators.  I have also conducted research on the use of a small fleet of autonomous underwater vehicles to search for and inspect mine-like objects in littoral regions; this research focused on facilitating communication and collaboration among the vehicles, while restricted by the extremely limited communications bandwidth.

A short summary of my various research topics is given below.


Goal Reasoning provides a method for creating autonomous agents that can reason about and adjust their goals during execution, allowing the agent to operate intelligently in changing and unexpected conditions.  The GRIM framework (Goal Reasoning with Information Measures) is a Goal Reasoning framework in which the goals are defined an evaluated with respect to the information measures that the agents use during execution of the goals.

Click here for an overview of GRIM.

LTL Playcalling

Linear Temporal Logic (LTL) is a logical formalism that can be used to specify temporal properties, and can be used to specify the behavior of autonomous systems.  This specification can then be used to generate a correct-by-construction controller for that system (i.e., the behavior of that controller is guaranteed under specific conditions).  This technique is extremely useful for behavior- or task-switching controllers, and can be used in a playcalling architecture to ensure that the system safely interprets externally supplied commands (analogous to “plays”) when switching its behavior.

Click here for more information on the LTL Playcalling architecture.

Probabilistic Guarantees for LTL Controllers

When synthesizing a robot controller from an LTL specification, the controller is guaranteed to satisfy the underlying specifications from which it was synthesized, assuming that it has perfect sensors and actuators.  This assumption, however, does not hold when applied to robots operating in the real world.  We can, however, evaluate the probabilistic performance of the robot by generating and model-checking a probabilistic model of the robot in its environment (complete with erroneous sensing and acting).  These results can then be used to inform design decisions and to adjust the underlying specification  to result in more desirable behavior.

Click here for more information on the probabilistic analysis of LTL-synthesized controllers.

UUV Communication and Cooperation

Teams of Unmanned Underwater Vehicles (UUVs) face a unique challenge in robotics: the environment in which they operate causes extremely slow and unreliable communications.  Because of this, it is essential to develop communication schemes and control algorithms that utilize only small amounts of communication between vehicles.  The schemes and algorithms allow a team of small UUVs to collaboratively search for, inspect, and map mine-like objects in littoral environments.

For more details on my research, please see my various publications.