A logical zonotope, which is a new set representation for binary vectors, is introduced in this paper. A logical zonotope is constructed by XOR-ing a binary vector with a combination of other binary vectors called generators. Such a zonotope can represent up to 2^n binary vectors using only n generators. It is shown that logical operations over sets of binary vectors can be performed on the zonotopes' generators and, thus, significantly reduce the computational complexity of various logical operations (e.g., XOR, NAND, AND, OR, and semi-tensor products). Similar to traditional zonotopes' role in the formal verification of dynamical systems over real vector spaces, logical zonotopes can be used to analyze discrete dynamical systems defined over binary vector spaces efficiently. We illustrate the approach and its ability to reduce the computational complexity in two use cases: (1) encryption key discovery of a linear feedback shift register and (2) safety verification of a road traffic intersection protocol.

翻译：本文提出了一种新型二进制向量集合表示——逻辑Zonotope。逻辑Zonotope通过将一个二进制向量与一组称为生成元的其他二进制向量的异或组合构建而成，仅需n个生成元即可表示多达2^n个二进制向量。研究表明，二进制向量集合上的逻辑运算可转化为对生成元的操作，从而显著降低各类逻辑运算（如异或、与非、与、或及半张量积）的计算复杂度。与传统Zonotope在实向量空间动力系统形式化验证中的作用类似，逻辑Zonotope可高效分析定义在二进制向量空间上的离散动力系统。我们通过两个用例验证该方法及其降低计算复杂度的能力：(1) 线性反馈移位寄存器的加密密钥发现；(2) 道路交通交叉口协议的安全性验证。