Eliminating Spurious Transitions in Reachability with Support Functions

Abstract

Computing an approximation of the reachable states of a hybrid system is a challenge, mainly because representing the solutions of ODEs with a finite number of sets does not scale well. Using template polyhedra to cover the solution greatly reduces the computational complexity, since it replaces complex operations on sets by a small number number of optimization problems. However, the use of templates may make the overapproximation too conservative. Spurious transitions (which are falsely considered reachable) are particularly detrimental to performance and accuracy, and may exacerbate the state explosion problem. In this paper, we examine how spurious transitions can be avoided with minimal computational effort. To this end, detecting spurious transitions is reduced to the well-known problem of showing that two convex sets are disjoint by finding a hyperplane that separates them. We generalize this to flowpipes by considering hyperplanes that evolve with time in correspondence to the dynamics of the system. The approach is implemented in the model checker SpaceEx and demonstrated on examples.