Skip to content

Signal temporal logic (STL) formulas and robustness in Julia

License

Notifications You must be signed in to change notification settings

sisl/SignalTemporalLogic.jl

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

22 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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

Pluto source Build Status

Installation

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

Examples

Pluto tests

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

About

Signal temporal logic (STL) formulas and robustness in Julia

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages