Unbounded-time reachability analysis of hybrid systems by abstract acceleration

Linear dynamical systems are ubiquitous in hybrid systems, both as physical models or as software control modules. Therefore we need an unbounded-time reachability analysis that can cope with industrial-scale hybrid system models with hundreds of variables. Abstract acceleration is a method developed for the unbounded-time polyhedral reachability analysis of linear software loops that has made promising progress in recent years. The method relies on a relaxation of the solution of the linear recurrence equation, leading to a precise convex over-approximation of the set of reachable states. It has been shown to be competitive with alternative approaches using set-based simulation or constraint solving. This paper explains the basic concepts of the technique, surveys recent advances of the technique towards the application to hybrid discrete and continuous-time linear dynamical systems, and formulates challenges to be tackled.