We discuss how to define a kernel for Signal Temporal Logic (STL) formulae. Such a kernel allows us to embed the space of formulae into a Hilbert space, and opens up the use of kernel-based machine learning algorithms in the context of STL. We show an application of this idea to a regression problem in formula space for probabilistic models.
Signal Temporal Logic (STL) [
Most of the applications of STL have been applied to deterministic (hybrid) systems, with less emphasis
on non-deterministic or stochastic ones [
In this work, we tackle the metric, learning, and model distance problems from a different perspective
than the classical one, which is based on some form of comparison of the languages of formulae. The
starting point is to consider an STL formula as a function mapping a real-valued trajectory (signal) into a
number or into another trajectory. As signals are functions, STL formulae should be properly considered
as functionals, in the sense of Functional Analysis (FA) [
A crucial aspect is that kernels for functionals are typically defined by integrating over the support space, with respect to a given measure. However, in trajectory space, there is no canonical measure (unless one discretizes time and maps signals to Rn), which introduces a degree of freedom on which measure to use. We decide to work with probability measures on trajectories, i.e. stochastic processes, and we build one that favours “simple” trajectories, with a small total variation. This encodes the idea that two formulae differing on simple signals should have a larger distance than two formulae differing only on complex trajectories. As we will see in the experiments, this choice allows the effective use of this kernel to perform regression on the formula space for approximating the satisfaction probability and the expected robustness of several stochastic processes, different than the one used to build the kernel. 1.1
Background
Signal Temporal Logic. (STL) [
ϕ := tt|μ|¬ ϕ|ϕ1 ∧ ϕ2|ϕ1U[a,b]ϕ2
where tt is the Boolean true constant, μ is an atomic predicate, negation ¬ and conjunction ∧ are the
standard Boolean connectives and U[a,b] is the until operator, with a, b ∈ R and a < b. As customary, we
can derive the disjunction operator ∨ and the future eventually F[t1,t2] and always G[t1,t2] operators from
the until temporal modality. The logic has two semantics: a Boolean semantics, ξ |= ϕ, with the meaning
that the trajectory ξ satisfies the formula ϕ and a quantitative semantics, ρ(ϕ, ξ), that can be used to
measure the quantitative level of satisfaction of a formula for a given trajectory. The function ρ is also
called the robustness function. The robustness is compatible with the Boolean semantics since it satisfies
the soundness property: if ρ(ϕ, ξ, t) > 0 then (ξ, t) |= ϕ; if ρ(ϕ, ξ, t) < 0 then (ξ, t) 6|= ϕ. Furthermore, it
satisfies also the correctness property, which shows that ρ measures how robust is the satisfaction of a
trajectory with respect to perturbations. We refer the reader to [
Given a stochastic process M = (T , A, μ), where T is a trajectory space and μ is a probability measure
on a σ-algebra A of T , we define the expected robustness as hρ(ϕ, t)i := E[ρ(ϕ, ξ, t)] = Rξ∈T ρ(ϕ, ξ, t)dμ(ξ).
The qualitative counterpart of the expected robustness is the satisfaction probability S(ϕ, t), i.e. the
probability that a trajectory generated by the stochastic process M satisfies the formula ϕ at the time
t: E[s(ϕ, ξ, t)] = Rξ∈T s(ϕ, ξ, t)dμ(ξ) where s(ϕ, ξ, t) = 1 if (ξ, t) |= ϕ and 0 otherwise. The satisfaction
probability S(ϕ, t) is the probability that a trajectory generated by the stochastic process M satisfies the
formula ϕ at the time t.
Kernel Functions. A kernel k(x, z), x, z ∈ X, defines an integral linear operator on functions X → R,
which intuitively can be thought of as a scalar product on a possibly infinite feature space F : k(x, z) =
hφ(x), φ(z)i, with φ : X → F being the eigenfunctions of the linear operator, spanning a Hilbert space,
see [
One application is kernel regression, with the goal of estimating the function f (x) = Ey[y|x] , x ∈ X, from a finite amount of observations {x1, ..., xN } ⊂ X, where each observation xi has an associated response yi ∈ R, and {(x1, y1), ..., (xN , yN )} is the training set. There exist several methods that address this problem, exploiting the kernel function k : X × X → R as a similarity measure between a generic x ∈ X and the observations {x1, ..., xN } of the training set. In the experiments, we compare different regression models used to compute the expected robustness and the probability satisfaction. 2
If we endow an arbitrary space with a kernel function, we can apply different kinds of regression methods.
Even for a non-metric space such as the STL formulae one, with a kernel we could perform operations
that are very expensive, such as the estimation of the satisfaction probability and the expected robustness
for a stochastic model of any formula ϕ, without running additional simulations. The idea behind our
definition is to exploit the robustness to project an STL formula to a Hilbert space, and then to compute
the scalar product in that space. In fact, the more similar the two projections will be, and the higher the
scalar product will result. In addition, the function that we will define will be a kernel by construction.
STL kernel. Let us fix a formula ϕ ∈ P in the STL formulae space. Consider the robustness ρ(ϕ, · , · ) :
T × I → R, I ⊂ R is a bounded interval, and T is the trajectory space of continuous functions. We
observe that there is a map h : P → C(T × I) defined by h(ϕ)(w, t) = ρ(ϕ, w, t). It can be proved that
h(P) ⊆ L2(T × I) [
h(ϕ)(ξ, t)h(ψ)(ξ, t)dtdμ0 = Z
Z ξ∈T t∈I
Z
Z
ξ∈T t∈I
ρ(ϕ, ξ, t)ρ(ψ, ξ, t)dtdμ0
The function k0 can be showed to satisfy the finitely positive semi-definite property and then it can be
proved that is a kernel itself [
One desirable property of our kernel is that k(ϕ, ϕ) ≥ k(ϕ, ψ) , ∀ϕ, ψ ∈ P. In fact, given a formula ϕ, no formula should be more similar to ϕ then ϕ itself. This property can be enforced by redefining the kernel as follows:
k(ϕ, ψ) = pk0(kϕ0,(ϕϕ),kψ0()ψ, ψ) .
The base measure μ0. In order to make our kernel meaningful and not too expensive to compute, we
endow the trajectory space T with a probability distribution such that more complex trajectories are less
probable. We use the total variation [
Kernel Regression on μ0. To show the goodness of our kernel definition, we use it to predict the
expected robustness and the satisfaction probability of STL formulae w.r.t. the stochastic process μ0
defined on T . We use a training set composed of 400 formulae sampled randomly according to a syntax
tree random growing scheme [
As it can be seen from Figure 2 (left), our base kernel is the best performing one. This can be explained by the fact that the measure μ0 is broad in terms of coverage of the trajectory space, meaning that different kinds of behaviours tend to be covered. This allows to better distinguish among STL formulae, compared to models that tend to focus the probability mass on narrower regions of T , such as the Isomerization model (which has the worst performance). Also in this case, we obtained the best results using SVR and KRR. However, given the sparseness of SVR, it’s more convenient to use it, since we need to evaluate a lower number of kernels to perform the regression. Interestingly, the minimum MSE is obtained using the Gaussian kernel with exactly the same σ parameter as for the regression task on μ0, hinting for some intrinsic robustness to hyperparameter’s choice that has to be investigated in greater detail. In Figure 2 (right) we show the predictions for the expected robustness over the three stochastic models that we took as examples, using the best regression model that we have found so far, which is the SVR with a Gaussian kernel having σ = 0.22. Note that to compute the kernel by Monte Carlo approximation, we have to sample only once the required trajectories for μ0. We also need to estimate the expected robustness transition probability for the formulae comprising the training set. However, kernel regression permits us to avoid further simulations of the model μ for novel formulae φ. 4
We defined a kernel for STL, fixing a base measure over trajectories, and we showed that we can use
exactly the same kernel across different stochastic models for computing a very precise approximation
of the expected robustness of new formulae, with only the knowledge of the expected robustness of a
fixed set of training formulae. Our STL-kernel, however, can also be used for other tasks. For instance,
computing STL-based distances among stochastic models, resorting to a dual kernel construction, and
building non-linear embeddings of formulae into finite dimensional real spaces with kernel-PCA techniques.
Another direction for future work is to refine the quantitative semantics in such a way that equivalent
formulae have the same robustness, e.g. using ideas like in [
Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications.