Taylor model flowpipe construction for non-linear hybrid systems

Verifying the safety of complex real-time control systems acting in a dynamic environment can be led back to the safety verification of hybrid systems. For this latter task we propose a novel approach based on Taylor models, which we
use to safely over-approximate smooth functions over bounded domains by a polynomial which is bloated by an interval. Besides the construction of flowpipes, which represent the continuous dynamics of the system, the main challenge lies in the handling of discrete (controller) transitions, for which we
explore various solutions based on two ideas: domain contraction and range over-approximation. Instead of explicitly computing the intersection of a Taylor model with a guard set, domain contraction makes the domain of a Taylor model smaller by cutting away parts for which the intersection is empty. It is complemented by range over-approximation that translates Taylor models into commonly used representations such as template polyhedra or zonotopes, on which intersections with guard sets have been previously studied. We demonstrate the advantages of our techniques on a set of challenging benchmarks.