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

Autor:	Hadjiloizou, Loizos, Jiang, Frank J., Alanwar, Amr, Johansson, Karl H.
Rok vydání:	2024
Předmět:	Electrical Engineering and Systems Science - Systems and Control Computer Science - Logic in Computer Science
Druh dokumentu:	Working Paper
Popis:	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. Comment: 6 pages, 3 figures, 1 table, 1 algorithm
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2404.03308 Zobrazit plný text záznamu View this record from Arxiv