论文标题
逻辑分子：布尔函数正式验证的集合表示
Logical Zonotopes: A Set Representation for the Formal Verification of Boolean Functions
论文作者
论文摘要
本文介绍了一种逻辑界限，它是二进制向量的新集表示。通过XOR-ing二进制向量与其他称为发电机的二进制向量组合来构建逻辑界限。这样的界限只能仅使用n发电机代表多达2^n二进制向量。结果表明，可以对二进制向量集的逻辑操作进行在Zonotopes的发电机上执行，因此可以显着降低各种逻辑操作的计算复杂性（例如XOR，NAND和OR和SEMI TENSOR产品）。类似于传统的地质植物在实际矢量空间上对动态系统的形式验证中的作用，逻辑界限可以有效地分析在二进制矢量空间上定义的离散动态系统。我们说明了在两种用例中降低计算复杂性的方法及其能力：（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.
