Reachability Analysis of Nonlinear Differential-Algebraic Systems

Abstract—This paper presents a numerical procedure for the reachability analysis of systems with nonlinear, semi-explicit, index-1 differential-algebraic equations. The procedure computes reachable sets for uncertain initial states and inputs in an overap-proximative way, i.e. it is guaranteed that all possible trajectories of the system are enclosed. Thus, the result can be used for formal verification of system properties that can be specified in the state space as unsafe or goal regions. Due to the representation of reachable sets by zonotopes and the use of highly scalable operations on them, the presented approach scales favorably with the number of state variables. This makes it possible to solve problems of industry-relevant size, as demonstrated by a transient stability analysis of the IEEE 14-bus benchmark problem for power systems. Index Terms—Reachability analysis, formal safety verification, nonlinear differential-algebraic equations (DAEs), zonotopes, power systems. I