A kernel function for Signal Temporal Logic formulae

Signal Temporal Logic (STL) [14] is gaining momentum as a requirement specification language for complex systems and, in particular, Cyber-Physical Systems [4]. STL has been applied in several flavours, from Runtime-monitoring [4] to control synthesis [10] and falsification problems [9], and recently also within learning algorithms, trying to find a maximally discriminating formula between sets of trajectories [5, 3, 16]. In these applications, a central role is played by the real-valued quantitative semantics [8], measuring robustness of satisfaction. Most of the applications of STL have been applied to deterministic (hybrid) systems, with less emphasis on non-deterministic or stochastic ones [2]. Another area in which formal methods are providing interesting tools is in logic-based distances between models, like bisimulation metrics for Markov models [1], which are typically based on a branching logic. In fact, extending these ideas to linear time logic is hard [7], and typically requires statistical approximations.