Transient stability analysis by reachable set computation

We present a formal technique for verifying the stability of transient responses of power systems. The procedure uses reachability analysis to compute the complete set of possible transient responses starting from a set of initial states, subject to a dynamics specified by differential-algebraic equations. The method is constructive and fully automatic, two properties that are often hard to achieve with direct Lyapunov methods when the differential-algebraic equations are not simplified. Reachability analysis is computationally expensive, but this work presents new techniques that make it possible to verify the stability of a transient response of the IEEE 14-bus benchmark power system network.