Polynomial Zonotopes Intersection Checking

1 Poster Description In the recent studies of formal verification of cyber-physical systems, polynomial zonotopes [1], a non-convex set representation, has brought new insights to the field. Comparing to previous set representations like zonotopes, which is a linear mapping of box domain, the polynomial mapping nature of polynomial zonotopes makes it has the ability to enclose the reachable set in a much tighter manner, (example shown in Fig.1). However, while the accuracy benefits from the nonlinear nature of the set, the cost of performing intersection checking increases due to the non-convexity. In this poster, we demonstrate our recent studies of polynomial zonotopes for reachable set computation and intersection checking analysis both theoretically and experimentally. First, we show the mathematical definition of the set representations and the accuracy benefits of polynomial zonotopes through a plotted figure of an example reachable set. Then we show that the cost of obtaining the accuracy benefits is transferred to the intersection checking problem, where we theoretically proved that it is NP-hard. And the existing algorithm for intersection checking for the polynomial zonotopes has non-monotonic convergence issue. To mitigate these issues, we research a modified version of the set representation to have arbitrary positive ranges such that it achieves a faster intersection checking speed experimentally and shows monotonic convergence for the intersection checking algorithm theoretically. This poster summarized our sequential work of [2-4] which are the sources of the content and figure.