SENTIL

A tool for Signal Temporal Logic and its Probabilistic extension, PrSTL. It monitors a signal in real time, checks a probabilistic specification, and synthesizes inputs and controllers that satisfy it.

Get started Open the playground Read the tutorial

Install

pip install sentil

cargo add sentil

vcpkg install sentil

vcpkg install sentil-cpp

<dependency>
  <groupId>io.github.sedislab</groupId>
  <artifactId>sentil</artifactId>
  <version>0.3.0</version>
</dependency>

] add Sentil

% after downloading Sentil.mltbx from the File Exchange or a GitHub release
matlab.addons.toolbox.installToolbox('Sentil.mltbx')

# macOS or Linux
brew install sedislab/sentil/sentil

# Windows
winget install SEDIS.SENTIL

# swap humble for jazzy or rolling
sudo apt install ros-humble-sentil-ros

Every package carries the compiled engine, so nothing above needs building. The install page adds the prerequisites, a check that each path landed, and the build from source. One page per language lives in the languages section, from install through the complete API.

Microcontrollers take a library through Arduino, PlatformIO, ESP-IDF, Zephyr, or a bare-metal archive. The Apollo module is source you drop into a workspace and build with Bazel, and the AUTOSAR Adaptive applications ship as packages that run against a stub or build against a vendor stack.

The first monitor

We monitor five samples of a speed signal against a specification. The speed dips to 4 at t=3 but the rule ask that speed be greater than 5, so the robustness is -1.

import sentil
from sentil import Formula

trace = sentil.Trace([0, 1, 2, 3, 4], {"speed": [12, 9, 7, 4, 6]})
phi = Formula.parse("G (speed > 5)")

print(phi.robustness(trace))  # -1.0

use sentil::{Formula, Trace};

fn main() -> sentil::Result<()> {
    let mut trace = Trace::new(vec![0.0, 1.0, 2.0, 3.0, 4.0])?;
    trace.add_signal("speed", vec![12.0, 9.0, 7.0, 4.0, 6.0])?;

    let phi = Formula::parse("G (speed > 5)")?;
    println!("robustness: {}", phi.robustness(&trace)?); // robustness: -1
    Ok(())
}

#include <stdio.h>
#include <sentil.h>

int main(void) {
    const double times[] = {0, 1, 2, 3, 4};
    const double speed[] = {12, 9, 7, 4, 6};
    sentil_trace_t *trace = sentil_trace_from_signal(times, 5, "speed", speed, 5);
    sentil_formula_t *phi = sentil_formula_parse("G (speed > 5)");
    double rho;
    if (!trace || !phi || sentil_formula_robustness(phi, trace, &rho) != SENTIL_OK) {
        fprintf(stderr, "%s\n", sentil_get_last_error());
        return 1;
    }
    printf("%f\n", rho);
    sentil_formula_destroy(phi);
    sentil_trace_destroy(trace);
    return 0;
}

-1.000000

#include <sentil/sentil.hpp>
#include <iostream>

int main() {
    sentil::Trace trace({0, 1, 2, 3, 4}, "speed", {12.0, 9.0, 7.0, 4.0, 6.0});
    sentil::Formula phi = sentil::Formula::parse("G (speed > 5)");

    std::cout << "robustness: " << phi.robustness(trace) << "\n";
    for (const sentil::Interval& v : phi.violations(trace)) {
        std::cout << "violation [" << v.start << ", " << v.end << "]\n";
    }
    return 0;
}

robustness: -1 violation [0, 3]

import io.github.sedislab.sentil.Formula;
import io.github.sedislab.sentil.Trace;

try (Trace trace = Trace.create(new double[] {0, 1, 2, 3, 4});
        Formula phi = Formula.parse("G (speed > 5)")) {
    trace.addSignal("speed", new double[] {12, 9, 7, 4, 6});
    System.out.println(phi.robustness(trace));   // -1.0
}

using Sentil

phi = formula("G (speed > 5)")
trace = Trace(collect(0.0:1.0:4.0), "speed", [12.0, 9.0, 7.0, 4.0, 6.0])
robustness(phi, trace)   # -1.0

trace = sentil.Trace([0 1 2 3 4], 'speed', [12 9 7 4 6]);
phi = sentil.Formula.parse('G (speed > 5)');

fprintf('robustness: %g\n', phi.robustness(trace));

robustness: -1

sentil check -f 'G (speed > 5)' -t speeds.csv

check formula G (speed > 5) trace speeds.csv semantics dense verdict violated robustness -1.000000

SENTIL

Install

The first monitor

Where to go

Monitor a signal

Verify under noise

Synthesize a controller

Reference