Flowpipe-guard intersection for reachability computations with support functions

Recently, efficient reachability algorithms for hybrid systems with piecewise affine dynamics have been developed. They achieve good scalability and precision by using support functions to represent continuous sets. In this paper, we propose an improvement of these algorithms that reduces the overapproximation error of the image computation of discrete transitions (jumps). The critical operation of this image computation is the intersection of the owpipe with the guard sets of the transitions, since intersection is in general a difficult operation when using support functions. We propose an approach for computing the intersection of the owpipe with polyhedral guards up to arbitrary accuracy. We reduce computing the support function of the intersection of a single convex set with a guard to a convex minimization problem. To solve it, we present a custom-tailored sandwich algorithm. The intersection of a owpipe (a sequence of convex sets) with a guard reduces to a set of such minimization problems. Where possible, we use branch-and-bound techniques and solve these minimization problems simultaneously to avoid redundant computations. Experimental results illustrate the gain in accuracy and the performance of the algorithms.