Fully Automated Verification of Linear Time-Invariant Systems Against Signal Temporal Logic Specifications via Reachability Analysis

This work presents a fully-automated verifier for linear time-invariant systems that can decide whether the system satisfies a given signal temporal logic (STL) specification for all initial states and uncertain inputs.