In this paper, we propose using constrained polynomial logical zonotopes for formal verification of logical systems. 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^n binary vectors using n 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. However, polynomial logical zonotopes are not closed under intersections. To address this, we formulate constrained polynomial logical zonotopes, which maintain the computational efficiency and exactness of polynomial logical zonotopes for reachability analysis while supporting exact intersections. Furthermore, we present an extensive empirical study illustrating and verifying the benefits of using constrained polynomial logical zonotopes for the formal verification of logical systems.

翻译：本文提出利用约束多项式逻辑Zonotope对逻辑系统进行形式化验证。我们通过可达性分析计算可能达到的状态集合。为此，采用近期提出的集合表示——多项式逻辑Zonotope，对逻辑系统执行计算高效且精确的可达性分析。值得注意的是，多项式逻辑Zonotope能够克服逻辑系统可达性分析中的“维度灾难”问题，因为该集合表示可用n个生成元表示2^n个二进制向量。完成可达性分析后，形式化验证涉及检验计算所得可达集与不安全集的交集是否为空。然而，多项式逻辑Zonotope对交集运算不封闭。针对这一问题，我们提出了约束多项式逻辑Zonotope，在保持多项式逻辑Zonotope进行可达性分析时计算高效性与精确性的同时，支持精确的交集运算。此外，我们通过大量实证研究展示并验证了将约束多项式逻辑Zonotope用于逻辑系统形式化验证的优势。