Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Reachability Analysis Using Constrained Polynomial Logical Zonotopes

Ahmad Hafez, Frank J. Jiang, Karl H. Johansson, Amr Alanwar

TL;DR

This work tackles reachability analysis for logical (Boolean) systems by introducing constrained polynomial logical zonotopes (CPLZ), which extend polynomial logical zonotopes with constraint structure to enable exact intersections without sacrificing efficiency. The framework defines comprehensive CPLZ set operations, including Minkowski and exact logical operations (XOR, AND, NOT, NAND, etc.), and proves exact intersection capabilities alongside computational complexity bounds. Through case studies, CPLZ demonstrate exact reachability in high-dimensional Boolean functions and outperform overapproximate methods and BDD-based approaches in scalability and precision. The proposed approach provides a practical, reproducible toolkit for robust formal verification of logical systems, with demonstrated improvements in accuracy of intersections and reachability sets.

Abstract

In this paper, we propose reachability analysis using constrained polynomial logical zonotopes. We perform reachability analysis to compute the set of states that could be reached. To do this, we utilize a recently introduced set representation called polynomial logical zonotopes for performing computationally efficient and exact reachability analysis on logical systems. Notably, polynomial logical zonotopes address the "curse of dimensionality" when analyzing the reachability of logical systems since the set representation can represent $2^h$ binary vectors using $h$ generators. After finishing the reachability analysis, the formal verification involves verifying whether the intersection of the calculated reachable set and the unsafe set is empty or not. Polynomial logical zonotopes lack closure under intersections, prompting the formulation of constrained polynomial logical zonotopes, which preserve the computational efficiency and exactness of polynomial logical zonotopes for reachability analysis while enabling exact intersections. Additionally, an extensive empirical study is presented to demonstrate and validate the advantages of constrained polynomial logical zonotopes.

Reachability Analysis Using Constrained Polynomial Logical Zonotopes

TL;DR

This work tackles reachability analysis for logical (Boolean) systems by introducing constrained polynomial logical zonotopes (CPLZ), which extend polynomial logical zonotopes with constraint structure to enable exact intersections without sacrificing efficiency. The framework defines comprehensive CPLZ set operations, including Minkowski and exact logical operations (XOR, AND, NOT, NAND, etc.), and proves exact intersection capabilities alongside computational complexity bounds. Through case studies, CPLZ demonstrate exact reachability in high-dimensional Boolean functions and outperform overapproximate methods and BDD-based approaches in scalability and precision. The proposed approach provides a practical, reproducible toolkit for robust formal verification of logical systems, with demonstrated improvements in accuracy of intersections and reachability sets.

Abstract

In this paper, we propose reachability analysis using constrained polynomial logical zonotopes. We perform reachability analysis to compute the set of states that could be reached. To do this, we utilize a recently introduced set representation called polynomial logical zonotopes for performing computationally efficient and exact reachability analysis on logical systems. Notably, polynomial logical zonotopes address the "curse of dimensionality" when analyzing the reachability of logical systems since the set representation can represent binary vectors using generators. After finishing the reachability analysis, the formal verification involves verifying whether the intersection of the calculated reachable set and the unsafe set is empty or not. Polynomial logical zonotopes lack closure under intersections, prompting the formulation of constrained polynomial logical zonotopes, which preserve the computational efficiency and exactness of polynomial logical zonotopes for reachability analysis while enabling exact intersections. Additionally, an extensive empirical study is presented to demonstrate and validate the advantages of constrained polynomial logical zonotopes.
Paper Structure (22 sections, 7 theorems, 31 equations, 2 tables)

This paper contains 22 sections, 7 theorems, 31 equations, 2 tables.

Table of Contents

  1. INTRODUCTION
  2. Problem Statement and Preliminaries
  3. Notation
  4. Preliminaries
  5. Problem Statement
  6. Constrained Polynomial Logical Zonotopes
  7. Set Operations
  8. Sets Intersection
  9. Logical Zonotopes Intersections
  10. Constrained Polynomial Logical Zonotopes Intersection
  11. Minkowski Logical Operations
  12. Minkowski XOR
  13. Minkowski AND
  14. Other Minkowski Operations
  15. Exact Logical Operations
  16. ...and 7 more sections

Key Result

Lemma 1

Given logical zonotopes $\mathcal{L}_1=\langle c_1, G_1\rangle$, and $\mathcal{L}_2=\langle c_2, G_2\rangle$ the intersection is overapproximated by $\mathcal{L}_{\cap} = \langle c_{\land},G_{\land} \rangle$ as follows. where $c_{\land} {=} c_{1} c_{2}$ and

Theorems & Definitions (11)

  • Definition 1: Minkowski XOR alanwar2022logical
  • Definition 2: Polynomial Logical Zonotope alanwar2023polynomial
  • Definition 3: Exact Reachable Set alanwar2022logical
  • Definition 4: Constrained Polynomial Logical Zonotope
  • Lemma 1
  • Lemma 2
  • Lemma 3
  • Lemma 4
  • Lemma 5
  • Lemma 6
  • ...and 1 more