Logical Zonotopes：一种用于布尔函数形式化验证的集合表示方法
Logical Zonotopes: A Set Representation for the Formal Verification of Boolean Functions
AI总结：
本文提出新型二元向量集合表示逻辑zonotope，可通过生成元执行逻辑运算以降低复杂度，适用于二元空间离散动力系统分析，并在密钥发现与交通协议安全验证场景中验证了效用。
摘要：
本文提出了一种针对二元向量的新型集合表示方法——logical zonotope（逻辑zonotope）。逻辑zonotope通过将一个二元向量与一组称为生成元的其他二元向量的组合进行异或（XOR）运算构建而成。这类zonotope仅需n个生成元，最多可表示2^n个二元向量。研究表明，针对二元向量集合的逻辑运算可直接在zonotope的生成元上执行，从而显著降低多种逻辑运算（如XOR、NAND、AND、OR以及半张量积）的计算复杂度。与传统zonotope在实向量空间上的动力系统形式化验证中发挥的作用类似，逻辑zonotope可高效分析定义在二元向量空间上的离散动力系统。我们通过两个用例验证了该方法及其降低计算复杂度的能力：（1）线性反馈移位寄存器的加密密钥发现；（2）道路交通交叉口协议的安全性验证。
英文摘要：
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 efficiently analyze discrete dynamical systems defined over binary vector spaces. 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
