stl2vec: Semantic and Interpretable Vector Representation of Temporal Logic

For algorithms is a longstanding challenge in Artificial Intelligence. Despite example in STL one can state properties like "the temperature of the the recognized importance of this task, a notable gap exists due room will reach 25 degrees within the next 10 minutes and will stay to the discreteness of symbolic representations and the continuous above 22 degrees for the next hour". In this area, one is typically interested nature of machine-learning computations. One of the desired bridges in understanding or verifying which properties the system between these two worlds would be to define semantically grounded under analysis is compliant to (or more precisely, in the probability vector representation (feature embedding) of logic formulae, thus enabling of observing behaviour satisfying the property). Such analysis is often to perform continuous learning and optimization in the semantic tackled by formal methods, via algorithms belonging to the world space of formulae. We tackle this goal for knowledge expressed in of quantitative model checking [4]. Signal Temporal Logic (STL) and devise a method to compute continuous In this work, we address the challenge of incorporating knowledge embeddings of formulae with several desirable properties: the in the form of temporal logic formulae inside data-driven embedding (i) is finite-dimensional, (ii) faithfully reflects the semantics learning algorithms. The key step is to devise a finite-dimensional of the formulae, (iii) does not require any learning but instead is embedding (feature mapping) of logical formulae into continuous defined from basic principles, (iv) is interpretable.