The first public release of SENTIL, a runtime verification and controller synthesis tool for Probabilistic Signal Temporal Logic.
SENTIL allows you to compute the robustness of a trace, offline or online, it also allows you to do probabilistic monitoring or monitoring of Probabilistic STL formulas. Finally, SENTIL allows you to turn a specification into a control input or an online controller. It is available in 7 languages and on 4 tools currently. Check the README for instructions as to how to install and sentil.pages.dev for tutorials.
Install
- Rust:
cargo add sentil - Python:
pip install sentil - Command line:
brew install sedislab/sentil/sentil, or scoop, winget, orcargo install sentil-cli - C and C++: the
.deband.rpmpackages and the platform tarballs attached below, or vcpkg and Conan - Java, Julia, MATLAB, ROS 2 and the embedded targets: see the per-package guides in the documentation
What is in it
- Online and offline STL and PrSTL monitoring.
- Statistical model checking with Wilson and Clopper-Pearson intervals, Chernoff-Hoeffding sample sizing, SPRT and Bayesian sequential tests, and adaptive multilevel splitting for rare events.
- Synthesis over smooth robustness, with a receding-horizon controller, chance constraints, witness and counterexample search, and a control-barrier-function safety filter.
- A specifications library of premade PrSTL formulas drawn from standards and papers
- ROS 2 packages for Humble, Jazzy, Kilted and Lyrical, an Apollo Cyber RT module, and an AUTOSAR Adaptive integration.
Reproducing the numbers
We make several claims about the correctness, speed and efficiency of SENTIL and we provide commands for reproducing all those claims in docs/CLAIMS.md.
Citing
The paper is on arXiv at arXiv:2605.21676. Use CITATION.cff for the entry.
SENTIL is by Paapa Kwesi Quansah and Ernest Bonnah at the SEDIS lab, Baylor University. Dual licensed under MIT or Apache-2.0.