STLmc: Robust STL Model Checking of Hybrid Systems Using SMT

EasyChair Preprint 8684

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

@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}}