Stefan Schupp: State Set Representations for Hybrid Systems Reachability Analysis

The increasing usage of digital systems to controll continuous processes has risen the need for formal verification of those hybrid systems, which combine discrete and continuous behavior. In my work I focus on flowpipe construction as one method to verify hybrid systems by means of reachability analysis. Flowpipe construction tries to over-approximate the set of reachable states of a given system by a set of geometric shapes for example boxes, convex polytopes, support functions or zonotopes. I have implemented and collected all of those state set representations in the publicly available open-source C++ library HyPro. To allow for modularized approaches indepentently of the state set representation we provide a unified interface of operations required for reachability analysis as well as several reduction and conversion techniques. Furthermore the library provides datastructures and utility functions for example required to set up a flowpipe-construction based reachability analysis algorithm.
To show applicability of the library I currently implement and maintain the reachability analysis tool HyDRA - not yet published -, which extends classical flowpipe-construction by several newly developed approaches. These include state set separation based on different dynamics, partial path refinement to falsify spurious counterexamples and most recently a parallelization of the whole approach.