  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.
