SignalTemporalLogic.jl

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).

Installation

] add https://github.com/sisl/SignalTemporalLogic.jl

Examples

See the tests for more elaborate examples: https://sisl.github.io/SignalTemporalLogic.jl/notebooks/runtests.html

Example STL formula

# 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)

Example robustness

# 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]

---

Robert Moss