In this paper, we propose reachability analysis using constrained polynomial logical zonotopes. We perform reachability analysis to compute the set of states that could be reached. To do this, we utilize a recently introduced set representation called polynomial logical zonotopes for performing 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.

翻译：本文提出了一种使用约束多项式逻辑Zonotopes的可达性分析方法。我们通过可达性分析来计算系统可能达到的状态集合。为此，我们利用一种新近提出的集合表示方法——多项式逻辑Zonotopes，以在逻辑系统上执行计算高效且精确的可达性分析。值得注意的是，多项式逻辑Zonotopes解决了逻辑系统可达性分析中的“维度灾难”问题，因为该集合表示法能够用 $h$ 个生成器表示 $2^h$ 个二进制向量。完成可达性分析后，形式化验证涉及验证计算出的可达集与不安全集的交集是否为空。多项式逻辑Zonotopes在交集运算下缺乏封闭性，这促使了约束多项式逻辑Zonotopes的构建。该表示法在保持多项式逻辑Zonotopes用于可达性分析的计算效率与精确性的同时，实现了精确的交集运算。此外，本文还提供了广泛的实证研究，以展示和验证约束多项式逻辑Zonotopes的优势。