Download PDFOpen PDF in browser

STLmc: Robust STL Model Checking of Hybrid Systems Using SMT

EasyChair Preprint no. 8684

13 pagesDate: August 16, 2022


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.

Keyphrases: model checking, Robustness degree, Signal Temporal Logic, SMT

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {Geunyeol Yu and Jia Lee and Kyungmin Bae},
  title = {STLmc: Robust STL Model Checking of Hybrid Systems Using SMT},
  howpublished = {EasyChair Preprint no. 8684},

  year = {EasyChair, 2022}}
Download PDFOpen PDF in browser