Reachability Analysis Using Constrained Polynomial Logical Zonotopes

This letter presents a novel approach for reachability analysis of using constrained polynomial logical zonotopes. We perform reachability analysis to compute the set of reachable states using a recently introduced set representation called polynomial logical zonotopes, enabling computationally efficient and exact reachability analysis on logical systems. Notably, polynomial logical zonotopes address the 'curse of dimensionality' when analyzing the reachability of logical systems since the set representation can represent 2^h binary vectors using h generators. After finishing the reachability analysis, the formal verification involves verifying whether the intersection of the calculated reachable set and the unsafe set is empty or not. Polynomial logical zonotopes lack closure under intersections, prompting the formulation of constrained polynomial logical zonotopes, which preserve the computational efficiency and exactness of polynomial logical zonotopes for reachability analysis while enabling exact intersections. Additionally, an extensive empirical study is presented to demonstrate and validate the advantages of constrained polynomial logical zonotopes.