Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes

In this talk, we will present the paper "Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes", accepted at TACAS 2022, the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, and nominated for a best-paper award. The paper introduces a similarity function on formulae of signal temporal logic (STL). The similarity function comes in the form of a kernel function, well known in machine learning as a conceptually and computationally efficient tool. The corresponding kernel trick allows us to circumvent the complicated process of feature extraction, i. e. the (typically manual) effort to identify the decisive properties of formulae so that learning can be applied. We demonstrate this consequence and its advantages on the task of predicting (quantitative) satisfaction of STL formulae on stochastic processes: Using our kernel and the kernel trick, we learn (i) computationally efficiently (ii) a practically precise predictor of satisfaction, (iii) avoiding the difficult task of finding a way to explicitly turn formulae into vectors of numbers in a sensible way. We back the high precision we have achieved in the experiments by a theoretically sound PAC guarantee, ensuring our procedure efficiently delivers a close-to-optimal predictor. We will discuss also the possible interesting applications of the technique. The main potential of our kernel (and generally introducing kernels for any further temporal logics) is that it opens the door to efficient learning on formulae via kernel-based machine-learning techniques. Other applications that immediately suggest themselves are: game-based synthesis, translating, sanitizing and simplifying specifications, and requirement mining.

Authors

• Laura Nenzi

Keywords

No keywords are indexed for this paper.