Template complex zonotopes: a new set representation for verification of hybrid systems
Arvind S. Adimoolam, Thao Dang · 2016
For most hybrid systems with non-trivial continuous dynamics, exact computation of trajectory sets is impossible, research efforts have thus put on finding good approximation methods. In program verification, this need also manifests, in particular in abstract interpretation which requires abstract domains which are expressive enough to accurately capture program executions, and yet computationally tractable to deal with complex programs. Two classical set representations are intervals and convex polyhedra [1], and their variants have been developed to achieve a good comprise between fast computational speed of the former domain and good accuracy of the latter, such as octagons [2], linear templates [3], zonotopes [4], and tropical polyhedra [5]. For hybrid model checking, convex polyhedra and their special classes such as parallelotopes and zonotopes, are also among the most popular data structures. They however have some inherent drawbacks, notably in approximation quality. Indeed, hybrid systems often generate complex sets of reachable states for which a single convex polyhedron is not sufficient to obtain an accurate approximation and very often many such polyhedra are required. This may lead to state-explosion problems since they are not closed under the union operation. Beyond polyhedral set representations, ellipsoids can be used for reachable set computations [6], [7], although they still suffer from state-explosion and over-approximation error. For invariant computation, polynomial inequalities are used via their reduction to linear inequalities in [8] and polynomial equalities via Groner basis method [9]. Quadratic templates using semi-definite relaxations is proposed, and this allows deriving non-linear (for instance quadratic inspired by Lyapunov functions) invariants [10], [11].