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.

Kyungmin Bae is an associate professor in the Department of Computer Science and Engineering at POSTECH (Pohang University of Science and Technology) in Korea. He received his Ph.D. in Computer Science from the University of Illinois at Urbana-Champaign. Before joining POSTECH, he worked as a postdoctoral researcher at Carnegie-Mellon University and SRI International. His current research interests are algorithmic verification techniques for cyber-physical systems, based on model checking, rewriting logic, and SMT.