| ||||
| ||||
![]() Title:STLmc: Robust STL Model Checking of Hybrid Systems Using SMT Conference:CAV 2022 Tags:Model checking, Robustness degree, Signal temporal logic and SMT Abstract: We 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. STLmc: Robust STL Model Checking of Hybrid Systems Using SMT ![]() STLmc: Robust STL Model Checking of Hybrid Systems Using SMT | ||||
Copyright © 2002 – 2025 EasyChair |