  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.
