A Study on Solving Guard and Invariant Set Intersection in Zonotope-based Reachability of Linear Hybrid Systems

Solving the problem of guard and invariant intersection when deciding for zonotopes to represent reachable sets of linear hybrid systems is still challenging. This is due to the fact that the intersection operation causes the loss of the zonotopic form. Furthermore a tradeoff must be found between computational efficiency and the tightness of the approximation. In this paper, we provide an overview, improve on some methods as well as carry out a comparative evaluation of different methods for zonotope/hyperplane intersection.These methods are then evaluated in combination with different clustering techniques in the context of guard intersection for the reachability analysis of two-tank and colliding-masses benchmarks. We thereafter propose zonotope/halfspace and zonotope/polyhedron intersection methods as solution for handling invariants inside continuous modes. Experimental evaluation however reveals that embedded in the reachability computational process, these methods do differ in performances as compared to when they are used as standalone functions.