In this paper, we introduce a set representation called polynomial logical zonotopes for performing exact and computationally efficient reachability analysis on logical systems. Polynomial logical zonotopes are a generalization of logical zonotopes, which are able to represent up to 2^n binary vectors using only n generators. Due to their construction, logical zonotopes are only able to support exact computations of some logical operations (XOR, NOT, XNOR), while other operations (AND, NAND, OR, NOR) result in over-approximations in the reduced space, i.e., generator space. In order to perform all fundamental logical operations exactly, we formulate a generalization of logical zonotopes that is constructed by dependent generators and exponent matrices. We prove that through this polynomial-like construction, we are able to perform all of the fundamental logical operations (XOR, NOT, XNOR, AND, NAND, OR, NOR) exactly in the generator space. While we are able to perform all of the logical operations exactly, this comes with a slight increase in computational complexity compared to logical zonotopes. We show that we can use polynomial logical zonotopes to perform exact reachability analysis while retaining a low computational complexity. To illustrate and showcase the computational benefits of polynomial logical zonotopes, we present the results of performing reachability analysis on two use cases: (1) safety verification of an intersection crossing protocol and (2) reachability analysis on a high-dimensional Boolean function. Moreover, to highlight the extensibility of logical zonotopes, we include an additional use case where we perform a computationally tractable exhaustive search for the key of a linear feedback shift register.

翻译：本文提出了一种称为多项式逻辑区域体的集合表示方法，用于对逻辑系统进行精确且计算高效的可达性分析。多项式逻辑区域体是逻辑区域体的推广形式，能够仅使用n个生成器表示多达2^n个二元向量。由于构造方式的限制，逻辑区域体仅支持部分逻辑运算（XOR、NOT、XNOR）的精确计算，而其他运算（AND、NAND、OR、NOR）在降维空间（即生成器空间）中会产生过近似。为了精确执行所有基本逻辑运算，我们通过引入依赖生成器和指数矩阵，构建了逻辑区域体的推广形式。我们证明，通过这种类多项式构造，能够在生成器空间中精确执行所有基本逻辑运算（XOR、NOT、XNOR、AND、NAND、OR、NOR）。尽管实现了所有逻辑运算的精确计算，但与逻辑区域体相比，计算复杂度略有增加。研究表明，在保持低计算复杂度的前提下，我们可以利用多项式逻辑区域体进行精确的可达性分析。为展示多项式逻辑区域体的计算优势，我们呈现了两个用例的可达性分析结果：（1）交叉路口通行协议的安全性验证，（2）高维布尔函数的可达性分析。此外，为突出逻辑区域体的可扩展性，我们补充了一个用例：对线性反馈移位寄存器的密钥进行计算可处理的穷举搜索。