Electrical and Computer Engineering ETDs

Publication Date

Fall 11-15-2018


Guaranteeing safety and performance are crucial components in any control system, and particularly relevant in light of growing interest in reliable autonomy. In safety-critical applications like biomedical devices, spacecraft applications, and self-driving cars, the cost of failure can be severe. Verification provides these guarantees by characterizing the ``good'' initial states or configurations from which a state can be driven to remain within a collection of pre-specified safe sets, while respecting the system dynamics, bounds on control authority, and additive uncertainties. We also wish to design controllers to achieve this objective. This dissertation proposes novel theory and scalable algorithms for tractable solutions to the stochastic reachability problems.

We treat the verification problems as backward stochastic reachability problems, since we wish to ascertain a set of initial states (back in time) that satisfy the pre-specified safety constraints in future and determine the associated admissible controllers. Current approaches to this problem are restricted to low dimensional systems since they rely on grids over the state space. In contrast, we have developed several approaches which avoid gridding, scale well with time and system dimension, and may be terminated at any time without compromising on the solution integrity (anytime algorithms). Additionally, our approaches enable controller synthesis that is open-loop or affine feedback. We design these algorithms by characterizing the sufficient conditions for the convexity and compactness of the sets. This enables verification of high-dimensional systems using convex optimization, stochastic programming, and Fourier transforms. We apply our methods to verification of spacecraft rendezvous, as well as to automated anesthesia delivery.

We also discuss a related problem of predicting the stochasticity of the state of the system at a future time, given an initial state --- the problem of forward stochastic reachability. We address this problem using Fourier transforms and computational geometry. Using forward stochastic reachability, we also introduce probabilistic occupancy functions to reason about collision probability and characterize keep-out sets for probabilistic safety. The applications include autonomous surveillance and stochastic motion planning problems.

We present an open-source MATLAB toolbox, SReachTools, that implements all the algorithms presented in this dissertation in an easily-accessible code base.


Control Theory, Optimization, Reachability, Stochastic Motion Planning, Stochastic Hybrid Systems

Document Type




Degree Name

Electrical Engineering

Level of Degree


Department Name

Electrical and Computer Engineering

First Committee Member (Chair)

Meeko Oishi

Second Committee Member

Chaouki Abdallah

Third Committee Member

Rafael Fierro

Fourth Committee Member

Lydia Tapia

Fifth Committee Member

Majeed Hayat