Reachability analysis of continuous dynamic systems using dimension reduction and decomposition

The computational complexity issue in reach set computation is one of the bottlenecks of current formal verification tools. This thesis presents methods to improve the efficiency of reach set computations for continuous dynamic systems. The methods developed in this thesis are based on model order reduction and decomposition techniques.;We present a method to compute the reach set for linear time-invariant systems using reduced-order models. Our method incorporates a new method for computing tight bound on the error introduced by reduced-order models and incorporates the bound into the reach set over-approximations.;We introduced a new representation for polytopes called affine representation, which enables efficient representation of low-dimensional polytopes. With the affine representation we developed a reach set computation procedure. We developed procedures to incorporate the computation method into C HECKMATE. Experiments show that using affine representations the computation time of the new procedures scales well with the order of the continuous dynamics, making it possible to extend the limit of current hybrid system verification tools. With the affine representations we developed a method to compute the reach sets for large-scale affine systems and a new method to compute over-approximations of the reach sets for nonlinear systems using trajectory piecewise-linear models. The efficiency of the method is demonstrated using transient stability assessment of a three-machine and ten-machine electric power networks.;We presented a method to compute reach sets for affine systems using epsilon-decomposition method. We showed that under certain conditions we are able to compute over-approximations of the reach sets of the system arbitrarily close to the actual reach sets.