Logical Zonotopes: A Set Representation for the Formal Verification of Boolean Functions

TL;DR

This paper introduces logical zonotopes, a novel set representation for binary vectors that enables efficient logical operations and analysis of discrete systems, demonstrated through cryptography and traffic safety verification.

Contribution

It presents the concept of logical zonotopes, allowing set operations on binary vectors to be performed efficiently, advancing formal verification methods for discrete systems.

Findings

Logical zonotopes can represent up to 2^n binary vectors with n generators.

Logical operations are efficiently performed on zonotope generators.

The approach reduces computational complexity in cryptography and safety verification tasks.

Abstract

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.