Eric M. Wolff — ResearchOverviewMy research interests span the areas of cyberphysical systems, robotics, and control theory. I am motivated by safety-critical applications involving autonomous air and ground vehicles carrying out complex tasks in uncertain and adversarial environments. Current methods for the specification, design, and verification of such hybrid (discrete and continuous state) dynamical systems are ad hoc and may lead to unexpected failures. I draw on ideas from optimization, hybrid systems, and model checking to develop formal methods for guaranteeing the correct behavior of such systems. BackgroundThe responsibilities we give to robots, autonomous vehicles, and other cyberphysical systems outpace our ability to reason about the correctness of their behavior. While we may tolerate unanticipated behavior and crashes from our personal computers and cell phones, the incorrect operation of autonomous vehicles could lead to significant loss of life and property. The increasingly tight integration of computation and control in complex systems (e.g., self-driving cars, unmanned aerial vehicles, human-robot teams, and embedded medical devices) often creates non-trivial failure modes. Thus, there is a growing need for formal methods to specify, design, and verify desired system behavior. I have focused my research on the specification and design of controllers that guarantee correct and efficient behaviors of robots, autonomous vehicles, and other cyberphysical systems. These systems need to accomplish complex tasks, e.g., follow the rules of the road, regulate a physiological process, or help a human assemble a part. Temporal logic is an expressive language that can be used to specify these types of complex tasks and properties. Such specifications generalize the classical notions of stability and reachability that are studied in the control and hybrid systems communities. Temporal logic is promising for specifying the combined digital and physical behavior of autonomous systems, in part due to its widespread use in software verification. Formal methods for the specification and verification of software have enjoyed enormous success in both academia and industry. However, formal synthesis of high-performance controllers for hybrid systems carrying out complex tasks in uncertain and adversarial environments remains an open problem. Major problems include the scalable and optimal synthesis of discrete supervisory controllers, and the computation of controllers (both feasible and optimal) for high-dimensional, nonlinear systems. With my advisor and collaborators, I have developed new techniques that help overcome these problems. I describe three highlights of my thesis work below. 1. Efficient and Optimal Reactive Control SynthesisOne aspect of my research has been identifying task specification languages that are both expressive and computationally efficient for controller synthesis. A controller that guarantees the correct operation of a system in the presence of a non-deterministic or stochastic environment is said to be reactive. Reactive controller synthesis is known to be intractable for linear temporal logic specifications. My work answered the following questions:
Standard approaches for reactive controller synthesis scale poorly with problem size. I discovered a class of specifications for which controllers can be synthesized in time linear, instead of doubly- exponential, in the length of the specification. This class is also expressive, and includes specifications such as safe navigation, response to the environment, stability, and surveillance. Specifically, one can compute reactive control policies for non-deterministic transition systems and Markov decision processes in time polynomial in the size of the system and specification. The algorithms I developed are computationally efficient in theory and practice. Additionally, the underlying ideas appear to extend in a variety of new directions, including incremental and modular synthesis. In this same setting, I also showed how to compute optimal control policies for a variety of relevant cost functions. My work identified several important cases when optimal policies (for average and minimax cost functions) can be computed in time polynomial in the size of the system and specification. This insight lets us address new classes of large-scale supervisory control problems that could not be explored before. 2. Automaton-Guided Control of Nonlinear SystemsAnother area of my research focused on controller design for high-dimensional and nonlinear dynamical systems with temporal logic specifications. Standard approaches are based on the computationally expensive process of computing a discrete abstraction, which is intractable for high-dimensional and nonlinear systems. I investigated the following question: Can one compute controllers without the expensive computation of a discrete abstraction? I showed how to use the automaton representing a specification to guide the computation of a feasible controller for discrete-time nonlinear systems. This method automatically decomposes reasoning about a complex task into a sequence of simpler constrained reachability problems. Thus, one can create controllers for any system for which solutions to constrained reachability problems can be computed, e.g., using tools from robotic motion planning and model predictive control. My approach avoids the expensive computation of a discrete abstraction and is easy to parallelize. Using this method lets us design controllers for nonlinear and high-dimensional (10+ continuous state) systems with temporal logic specifications, something that was previously not possible. 3. Optimal Control of Nonlinear SystemsAnother facet of my research was creating optimal control policies for high-dimensional and non- linear dynamical systems. I answered the following question: How can one compute optimal control policies for nonlinear systems with temporal logic specifications? I developed an encoding of temporal logic specifications as mixed-integer linear constraints on a dynamical system. This generalizes previous Boolean satisfiability encodings of temporal logic specifications for finite, discrete systems. My approach directly encodes a linear temporal logic specification as mixed-integer linear constraints on the continuous system variables. The direct encoding of the specification avoids the expensive computations of a finite abstraction of the system and an automaton for the specification. Numerical experiments show that this approach scales to previously intractable temporal logic planning problems involving quadrotor and aircraft models. |