Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formal Verification of Linear Temporal Logic Specifications Using Hybrid Zonotope-Based Reachability Analysis

Loizos Hadjiloizou, Frank J. Jiang, Amr Alanwar, Karl H. Johansson

TL;DR

This work addresses formal verification of autonomous systems under LTL specifications in environments featuring non-convex, disjoint geometries. It introduces a hybrid zonotope (HZ) based backward reachability framework to construct Temporal Logic Trees (TLTs) efficiently, avoiding the computational burden of full level-set methods while capturing complex geometries. The method maps LTL operators to HZ operations (union, intersection, predecessor, and RCI) and leverages an augmented-state BRA to compute the reachable sets needed for TLT construction. A simulated parking scenario demonstrates the approach on five disjoint parking spots, achieving convergence in a modest runtime and illustrating the ability to handle disjoint geometries and non-convex regions. The results indicate practical potential for formal verification and online planning in complex, real-world environments.

Abstract

In this paper, we introduce a hybrid zonotope-based approach for formally verifying the behavior of autonomous systems operating under Linear Temporal Logic (LTL) specifications. In particular, we formally verify the LTL formula by constructing temporal logic trees (TLT)s via backward reachability analysis (BRA). In previous works, TLTs are predominantly constructed with either highly general and computationally intensive level set-based BRA or simplistic and computationally efficient polytope-based BRA. In this work, we instead propose the construction of TLTs using hybrid zonotope-based BRA. By using hybrid zonotopes, we show that we are able to formally verify LTL specifications in a computationally efficient manner while still being able to represent complex geometries that are often present when deploying autonomous systems, such as non-convex, disjoint sets. Moreover, we evaluate our approach on a parking example, providing preliminary indications of how hybrid zonotopes facilitate computationally efficient formal verification of LTL specifications in environments that naturally lead to non-convex, disjoint geometries.

Formal Verification of Linear Temporal Logic Specifications Using Hybrid Zonotope-Based Reachability Analysis

TL;DR

This work addresses formal verification of autonomous systems under LTL specifications in environments featuring non-convex, disjoint geometries. It introduces a hybrid zonotope (HZ) based backward reachability framework to construct Temporal Logic Trees (TLTs) efficiently, avoiding the computational burden of full level-set methods while capturing complex geometries. The method maps LTL operators to HZ operations (union, intersection, predecessor, and RCI) and leverages an augmented-state BRA to compute the reachable sets needed for TLT construction. A simulated parking scenario demonstrates the approach on five disjoint parking spots, achieving convergence in a modest runtime and illustrating the ability to handle disjoint geometries and non-convex regions. The results indicate practical potential for formal verification and online planning in complex, real-world environments.

Abstract

In this paper, we introduce a hybrid zonotope-based approach for formally verifying the behavior of autonomous systems operating under Linear Temporal Logic (LTL) specifications. In particular, we formally verify the LTL formula by constructing temporal logic trees (TLT)s via backward reachability analysis (BRA). In previous works, TLTs are predominantly constructed with either highly general and computationally intensive level set-based BRA or simplistic and computationally efficient polytope-based BRA. In this work, we instead propose the construction of TLTs using hybrid zonotope-based BRA. By using hybrid zonotopes, we show that we are able to formally verify LTL specifications in a computationally efficient manner while still being able to represent complex geometries that are often present when deploying autonomous systems, such as non-convex, disjoint sets. Moreover, we evaluate our approach on a parking example, providing preliminary indications of how hybrid zonotopes facilitate computationally efficient formal verification of LTL specifications in environments that naturally lead to non-convex, disjoint geometries.
Paper Structure (17 sections, 10 equations, 3 figures, 2 tables, 1 algorithm)

This paper contains 17 sections, 10 equations, 3 figures, 2 tables, 1 algorithm.

Table of Contents

  1. INTRODUCTION
  2. PRELIMINARIES
  3. Notation
  4. Plant Model
  5. Reachability Analysis
  6. Linear Temporal Logic
  7. Temporal Logic Tree
  8. Problem Statement
  9. Constructing TLTs using Hybrid Zonotopes
  10. Hybrid Zonotopes
  11. TLT Construction
  12. SIMULATED PARKING SCENARIO
  13. Vehicle Model
  14. Parking Environment
  15. Constructing the TLTs
  16. ...and 2 more sections

Figures (3)

  • Figure 1: We illustrate an overview of our approach.
  • Figure 2: TLT to check if the vehicle can eventually park.
  • Figure 3: Evolution of BRS from parking spots

Theorems & Definitions (8)

  • Definition II.1
  • Definition II.2
  • Definition II.3
  • Example II.1
  • Definition IV.1
  • Definition IV.2
  • Definition IV.3
  • Example IV.1