Download PDFOpen PDF in browser

STLmc: Robust STL Model Checking of Hybrid Systems Using SMT

EasyChair Preprint 8684

13 pagesDate: August 16, 2022

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.

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

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