Computing maximizer trajectories of affine dynamics for reachability

Computing an overapproximation of the reachable set of states of a continuous or hybrid system is a challenging problem. The use of overapproximations based on a set of template directions has led to scalable algorithms. When the approximation is too conservative, it can be refined by adding more template directions. Synthesizing suitable directions is possible but costly without tight underapproximations to guide the refinement. Suitable underapproximations can be constructed from the trajectories of states that are maximal in the template directions, which we call maximizers. In this paper, we propose algorithms to compute maximizer trajectories for dynamical systems with affine dynamics and nondeterministic inputs. Our computations are based solely on solving ODEs and, assuming the initial condition is a polytope, solving linear programs. Highly optimized commercial tools are available for both tasks, with corresponding performance and numerical robustness, which may help pave the way towards industrial applications of reachability analysis. Since maximizer trajectories represent actual executions of the system, or parts thereof, they can be used as counterexamples and provide additional feedback and insight to the user.