Talk "SMT-Based Model Checking for Signal Temporal Logic"

by Kyungmin Bae

Fri, 01 November 2024 at 02:30 pm in Crete, Greece

Joint work with: Jia Lee and Geunyeol Yu

Abstract: Signal Temporal Logic (STL) is a temporal logic formalism used to specify linear-time properties of continuous signals. STL has been widely applied in specifying, monitoring, and testing properties of hybrid systems that exhibit both discrete and continuous behavior. However, model checking techniques for hybrid systems have primarily been limited to invariant and reachability properties. This limitation arises from the intrinsic nature of hybrid systems, which involve uncountably many signals that continuously change over time. For hybrid systems, checking whether all possible behaviors satisfy an STL formula requires a certain form of abstraction and discretization, which has not been much studied for general STL properties. In this talk, I introduce a bounded model checking approach for general STL properties of hybrid systems. The core of our approach is built on a novel logical foundation for STL, which includes: (i) syntactic separation, which decomposes an STL formula into components, each depending exclusively on separate segments of a signal; (ii) signal discretization, which ensures a complete abstraction of a signal through a set of discrete elements; and (iii) epsilon-strengthening, which reduces robust STL model checking to Boolean STL model checking. With this foundation, the STL model checking problem---up to given bound parameters and robustness threshold---can be transformed into the satisfiability of a first-order logic formula, which is decidable if the reachability of the underlying hybrid system is decidable.