Get started
Welcome to SENTIL
SENTIL is a tool for Signal Temporal Logic and its Probabilistic extension, PrSTL.
New to Signal Temporal Logic? Read what STL is first, then come back here.
Install
Get SENTIL for your language.
pip install sentil
Your first monitor
Parse a formula, evaluate it, and read the robustness value quickly.
Start here
Monitor a signal
Write an STL formula and read quantitative robustness over a trace, online or offline.
The runtime monitor
Verify under noise
Lift noisy readings into a fitted distribution and estimate satisfaction probability.
The statistical layer
Synthesize a controller
Turn a specification into an input sequence or a feedback controller.
From spec to controller
Where to go next
Monitor a live stream
Feed samples one at a time and watch the verdict resolve as the window fills.
Run on a recorded trace
Load a CPS trace from a file and locate the interval where the property fails.
Learn interactively
Work one trace through predicates, booleans, and the temporal operators with every value checked by hand.
Troubleshooting
The errors a first run tends to hit, and the one-line fix for each.