Invited Talk

stl2vec:
Semantic Preserving Embeddings of Signal Temporal Logic
Luca Bortolussi
University of Trieste, Italy

Signal temporal logic is a powerful formalism to reason about real-time systems. Recently, a lot of work has
been channeled towards requirement mining, i.e., the goal of learning STL specifications from data or from
models. All these approaches, at least those not restricting to pre-specified templates, are substantially
based on operations that manipulate the syntax of a formula. Yet it’s the semantics of the logic that
carries the information that is needed. At the same time, the recent explosion of machine learning and
deep learning showed that working with real vectors is much easier, and brought several strategies to learn
encoding of combinatorial structures into a real feature space. In this talk, we will explore this direction
for STL, taking however an approach that avoids to introduce uncontrollable approximations due to the
use of neural networks, instead proposing an embedding based on suitable kernel functions. We will show
how to construct implicit and explicit embeddings with a controllable quality (in a probabilistic sense)
and test their quality on the problem of using machine learning to predict the result of model checking in
a stochastic setting (i.e., to predict satisfaction probability of properties).