Logical-Zonotope: A MATLAB repository from aalanwar

Logical Zonotope and polynomial logical zonotopes: Set Representations for Binary Vectors

This repo cotains the code for our two papers:

1- Polynomial Logical Zonotopes: A Set Representation for Reachability Analysis of Logical Systems
Authors: Amr Alanwar, Frank J. Jiang, and Karl Henrik Johansson

1- Logical Zonotope: A Set Representation for the Formal Verification of Boolean Functions
Authors: Amr Alanwar, Frank J. Jiang, Samy Amin and Karl Henrik Johansson

CDC 2023 talk

International Online Seminar on Interval Methods in Control Engineering

Abstract

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^\gamma$ binary vectors using only $\gamma$ 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 order to perform all fundamental logical operations
exactly, we formulate a generalization of logical zonotopes that is constructed by
additional 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. 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, (2) and 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.

Running

1- Add the repo folder and subfolders to the Matlab path.
2- Run TestLogicalFunctions.m for doing logical functions in the generator space of logical zonotope
3- Run TestPolyLogicalFunctions.m for doing logical functions in the generator space of polynomial logical zonotope
4- Run FindLFSRkeyExample.m for finding the key example in the papers
5- Run VechIntersection4Cars.m for the vehicle Intersections in the papers
6- Run BoolFunctionExample.m for the high dimensional Boolean function in the paper

Main Support APIs

Z = xor(Z1,Z2): XOR between two logical zontoopes or polynomial logical zonotopes
Z = and(Z1,Z2): AND between two logical zontoopes or polynomial logical zonotopes
Z = or(Z1,Z2): OR between two logical zontoopes or polynomial logical zonotopes
Z = nor(Z1,Z2): NOR between two logical zontoopes or polynomial logical zonotopes
Z = nand(Z1,Z2): NAND between two logical zontoopes or polynomial logical zonotopes
Z = not(Z1): not a logical zontoope or polynomial logical zonotope
Z = semiKron(Z1,Z2): Semi Tensor Produce between Z1 and Z2
Flag = Z.containPoints(P): Determines if the point p is inside the logical zonotope Z
Z = enclosePoints(points): Encloses points with a logical zonotope Z
Zred = reduce(Z): Reduces the number of generators of a logical zonotope

@article{alanwar2023polynomial,
  title={Polynomial Logical Zonotopes: A Set Representation for Reachability Analysis of Logical Systems},
  author={Alanwar, Amr and Jiang, Frank J and Johansson, Karl H},
  journal={arXiv preprint arXiv:2306.12508},
  year={2023}
}