A Logical Product Approach to Zonotope Intersection

By Khalil Ghorbal, É. Goubault, Sylvie Putot. 2010

54 citations recorded by the source corpus.

We define and study a new abstract domain which is a fine-grained combination of zonotopes with (sub-)polyhedric domains such as the interval, octagon, linear template or polyhedron domains While abstract transfer functions are still rather inexpensive and accurate even for interpreting non-linear computations, we are able to also interpret tests (i.e intersections) efficiently This fixes a known drawback of zonotopic methods, as used for reachability analysis for hybrid systems as well as for invariant generation in abstract interpretation: intersection of zonotopes are not always zonotopes, and there is not even a best zonotopic over-approximation of the intersection We describe some examples and an implementation of our method in the APRON library, and discuss some further interesting combinations of zonotopes with non-linear or non-convex domains such as quadratic templates and maxplus polyhedra.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Citations in the corpus

AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation (2018, methodology): “One way to compute a meet between a zonotope and a linear constraint is to modify the intervals of the error terms (see [11]).”
Robustness Analysis of Finite Precision Implementations (2013, unknown): “The computation of upper bounds (and if possible minimal ones) on constrained aﬃne sets is a diﬃcult task, already discussed in several papers [14,15,10,11], and orthogonal to the robustness analysis presented here.”