TY - GEN
T1 - Formal Verification of Linear Temporal Logic Specifications Using Hybrid Zonotope-Based Reachability Analysis
AU - Hadjiloizou, Loizos
AU - Jiang, Frank J.
AU - Alanwar, Amr
AU - Johansson, Karl H.
N1 - Publisher Copyright:
© 2024 EUCA.
PY - 2024
Y1 - 2024
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85200604183&partnerID=8YFLogxK
U2 - 10.23919/ECC64448.2024.10590925
DO - 10.23919/ECC64448.2024.10590925
M3 - Conference contribution
AN - SCOPUS:85200604183
T3 - 2024 European Control Conference, ECC 2024
SP - 579
EP - 584
BT - 2024 European Control Conference, ECC 2024
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 2024 European Control Conference, ECC 2024
Y2 - 25 June 2024 through 28 June 2024
ER -