Download PDFOpen PDF in browserSTLmc: Robust STL Model Checking of Hybrid Systems Using SMTEasyChair Preprint 868413 pages•Date: August 16, 2022AbstractWe present the STLmc model checker for signal temporal logic (STL) properties of hybrid systems. STLmc can perform STL model checking up to a robustness threshold for a wide range of nonlinear hybrid systems with ordinary differential equations. Our tool utilizes the refutation-complete SMT-based model checking algorithm with various SMT solvers by reducing the robust STL model checking problem into the Boolean STL model checking problem. If STLmc does not find a counterexample, the system is guaranteed to be correct up to the given bounds and robustness threshold. We demonstrate the effectiveness of STLmc on a number of hybrid system benchmarks. Keyphrases: Robustness degree, SMT, Signal Temporal Logic, model checking
|