STLmc: Robust STL Model Checking of Hybrid Systems Using SMT

Abstract

Abstract We present theSTLmcmodel checker for signal temporal logic (STL) properties of hybrid systems. TheSTLmctool can perform STL model checking up to a robustness threshold for a wide range of hybrid systems. Our tool utilizes the refutation-complete SMT-based bounded model checking algorithm by reducing the robust STL model checking problem into Boolean STL model checking. IfSTLmcdoes not find a counterexample, the system is guaranteed to be correct up to the given bounds and robustness threshold. We demonstrate the effectiveness ofSTLmcon a number of hybrid system benchmarks.