Abstraction based reachability computation for affine systems with bounded input

Reachability computation is the central problem of verification of hybrid or continuous systems. One approach, among others, to compute an over approximation of the reachable space is to split the continuous state space and to abstract the continuous dynamics in each cell by a linear differential inclusion for which the reachable space may be computed with polyhedra. Previous works proposed to use characteristics of the affine continuous dynamics to guide the decomposition and this paper considers the extension of this approach to systems with bounded input. It is shown that considering the vertices of the boundary of the input domain, the decomposition is still useful to perform the reachability analysis. An algorithm is then proposed and exemplified