This package can define signal temporal logic (STL) formulas using the @formula macro and then check if the formulas satisfy a signal trace. It can also measure the robustness of a trace through an STL formula and compute the gradient of the robustness (as well as an approximate gradient using smooth min and max functions).
] add SignalTemporalLogic
See the tests for more elaborate examples: https://sisl.github.io/SignalTemporalLogic.jl/notebooks/runtests.html
# Signals (i.e., trace)
x = [-0.25, 0, 0.1, 0.6, 0.75, 1.0]
# STL formula: "eventually the signal will be greater than 0.5"
ϕ = @formula ◊(xₜ -> xₜ > 0.5)
# Check if formula is satisfied
ϕ(x)# Signals
x = [1, 2, 3, 4, -9, -8]
# STL formula: "eventually the signal will be greater than 0.5"
ϕ = @formula ◊(xₜ -> xₜ > 0.5)
# Robustness
ρ(x, ϕ)
# Outputs: 3.5
# Robustness gradient
∇ρ(x, ϕ)
# Outputs: [0.0 0.0 0.0 1.0 0.0 0.0]
# Smooth robustness gradient
∇ρ̃(x, ϕ)
# Outputs: [-0.0478501 -0.0429261 0.120196 0.970638 -1.67269e-5 -4.15121e-5]