Publication Date


Document Type


Committee Members

Matthew Clark (Committee Member), Kuldip Rattan (Advisor), Xiaodong Zhang (Committee Member)

Degree Name

Master of Science in Engineering (MSEgr)


Systems that are modeled by non-linear continuous-time differential equations with uncertain parameters have proven to be exceptionally difficult to formally verify. The past few decades have produced a number of useful verification tools which can be applied to such systems but each is applicable to only a subset of possible verification scenarios. The Level Sets Toolbox (LST) is one such tool which is directly applicable to non-linear systems, however, it is limited to systems of relatively small continuous state space dimension. Other tools such as PHAVer and the SpaceEx invariant of the Le Guernic-Girard (LGG) support function algorithm are specifically designed for hybrid systems with linear dynamics and linear constraints but can accommodate hundreds of continuous states. The application of these linear reachability tools to non-linear models has been achieved by approximating non-linear systems as linear hybrid automata (LHA). Unfortunately, the practical applicability and limitations of this approach are not yet well documented. The purpose of this thesis is to evaluate the performance and dimensionality limitations of PHAVer and the LGG support function algorithm when applied to a LHA approximation of a particular non-linear system. A collision avoidance scenario with autonomous differential drive robots is used as a case study to demonstrate that an over-approximated reachable set boundary can be generated and implemented as a run time safety assurance mechanism.

Page Count


Department or Program

Department of Electrical Engineering

Year Degree Awarded


Creative Commons License

Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 License
This work is licensed under a Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 License.