TY - GEN

T1 - Logical Zonotopes

T2 - 62nd IEEE Conference on Decision and Control, CDC 2023

AU - Alanwar, Amr

AU - Jiang, Frank J.

AU - Amin, Samy

AU - Johansson, Karl H.

N1 - Publisher Copyright:
© 2023 IEEE.

PY - 2023

Y1 - 2023

N2 - A logical zonotope, which is a new set representation for binary vectors, is introduced in this paper. A logical zonotope is constructed by XORing a binary vector with a combination of other binary vectors called generators. Such a zonotope can represent up to 2γ binary vectors using only γ 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.

AB - A logical zonotope, which is a new set representation for binary vectors, is introduced in this paper. A logical zonotope is constructed by XORing a binary vector with a combination of other binary vectors called generators. Such a zonotope can represent up to 2γ binary vectors using only γ 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.

UR - http://www.scopus.com/inward/record.url?scp=85184806966&partnerID=8YFLogxK

U2 - 10.1109/CDC49753.2023.10384037

DO - 10.1109/CDC49753.2023.10384037

M3 - Conference contribution

AN - SCOPUS:85184806966

T3 - Proceedings of the IEEE Conference on Decision and Control

SP - 60

EP - 66

BT - 2023 62nd IEEE Conference on Decision and Control, CDC 2023

PB - Institute of Electrical and Electronics Engineers Inc.

Y2 - 13 December 2023 through 15 December 2023

ER -