Bounded STL Model Checking for Hybrid Systems (Invited Talk)

Abstract

Signal temporal logic (STL) is a temporal logic formalism for specifying properties of continuous signals. STL has been widely used for specifying, monitoring, and testing properties of hybrid systems that exhibit both discrete and continuous behavior. However, model checking techniques for hybrid systems have been primarily limited to invariant and reachability properties. This is mainly due to 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 developed for general STL properties.

In this talk, I introduce bounded model checking algorithms and tools for general STL properties of hybrid systems. Central to our technique is a novel logical foundation for STL: (i) a syntactic separation of STL, which decomposes an STL formula into components, with each component relying exclusively on separate segments of a signal, and (ii) a signal discretization, which ensures a complete abstraction of a signal, given by a set of discrete elements. With this new foundation, the STL model checking problem can be reduced to the satisfiability of a first-order logic formula. This allows us to develop the first model checking algorithm for STL that can guarantee the correctness of STL up to given bound parameters, and a pioneering bounded model checker for hybrid systems, called STLmc.