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

This work introduces a hybrid zonotope-based approach for efficiently verifying the behavior of autonomous systems operating under Linear Temporal Logic (LTL) specifications by constructing temporal logic trees (TLTs) via backward reachability analysis.