mstlo

mstlo (mistletoe) is a Rust library for online monitoring of Signal Temporal Logic (STL) specifications. It is designed for high performance and low memory usage, making it suitable for real-time monitoring of Cyber-Physical Systems. Python bindings are published as mstlo-python.

• mstlo
  • Features
  • Installation
  • Usage
    • Rust
    • Python
  • Documentation
  • Building from Source
  • Citing
  • License

Features

• Embedded DSL: the stl! macro embeds specifications in Rust and syntax-checks them at compile time.
• Unified semantics interface: delayed qualitative, delayed quantitative, eager qualitative and Robust Satisfaction Intervals (RoSI) behind a single monitor API.
• Dense-time signals: samples may arrive at arbitrary, irregular timestamps, per signal, with zero-order hold or linear interpolation between them.
• Python bindings: the mstlo-python package (import name mstlo_python) enables interactive workflows, e.g. in Jupyter notebooks.
• High performance: benchmarks show throughput exceeding existing state-of-the-art tools.

Installation

Rust:

cargo add mstlo

Python:

pip install mstlo-python

Usage

Rust

The monitor is configured with a builder, then fed samples as they arrive. This monitors G[0, 2](x > 5) ("x stays above 5 for the next two seconds") under RoSI semantics:

use mstlo::monitor::{Rosi, StlMonitor};
use mstlo::{step, stl};

fn main() {
    // Define a formula using the embedded DSL
    let formula = stl! {G[0, 2](x > 5.0)};

    // Build the monitor
    let mut monitor = StlMonitor::builder()
        .formula(formula)
        .semantics(Rosi)
        .build()
        .expect("Failed to build monitor");

    // Feed data steps to the monitor
    let out1 = monitor.update(&step!("x", 7.0, 0s));
    println!("{:?}", out1.verdicts());
    // [Step { signal: "x", value: RobustnessInterval(-inf, 2.0), timestamp: 0ns }]
    // at time 0, the robustness value is in the interval (-inf, 2.0)

    let out2 = monitor.update(&step!("x", 4.0, 1s));
    println!("{:?}", out2.verdicts());
    // [Step { signal: "x", value: RobustnessInterval(-inf, -1.0), timestamp: 0ns },
    //  Step { signal: "x", value: RobustnessInterval(-inf, -1.0), timestamp: 1s }]
    // early violation detection for times 0 and 1
}

Whole traces can also be fed at once with update_batch and the steps! macro, see Batch Updates. More examples are in mstlo/examples.

Python

import mstlo_python as mstlo

# Parse formula using the DSL syntax
phi = mstlo.parse_formula("G[0, 10](x > 5)")

# Create a monitor using the selected semantics
monitor = mstlo.Monitor(phi, semantics="Rosi")

# Update the monitor with streaming data (signal_name, value, timestamp)
output = monitor.update("x", 6.0, 0.5)
print(f"Verdicts: {output.verdicts()}")
# Verdicts: [(0.5, (-inf, 1.0))]  # (timestamp, (lower_bound, upper_bound) for robustness)

output = monitor.update("x", 3.0, 1.2)
print(f"Verdicts: {output.verdicts()}")
# Verdicts: [(0.5, (-inf, -2.0)), (1.2, (-inf, -2.0))]  # early indication of violation

More examples, including a notebook comparing the semantics, are in mstlo-python/examples.

Documentation

• Signal Temporal Logic and Evaluation Semantics: the supported STL syntax and the formal definitions of the four semantics.
• Implementation: the signal model, how input is consumed, when verdicts are emitted, and settings that can hurt performance.
• Rust API reference: docs.rs/mstlo
• Python API reference: INTO-CPS-Association.github.io/mstlo

Building from Source

Prerequisites: Rust (stable toolchain), and for the Python bindings Python 3.9+ and maturin.

git clone https://github.com/INTO-CPS-Association/mstlo.git
cd mstlo
cargo test -p mstlo
cargo run -p mstlo --example intro_example

Python bindings, from the repository root:

cd mstlo-python
pip install maturin pytest
maturin develop
pytest

Citing

If you use mstlo in your research, please cite the following paper:

@InProceedings{10.1007/978-3-032-41160-0_2,
  author = {Thomsen, Andreas Kaag and Madsen, Niels Viggo Stark and Evans, Valdemar Tang and Wright, Thomas and Esterle, Lukas and Larsen, Peter Gorm},
  title = {mstlo: Efficient Online Monitoring of Signal Temporal Logic},
  booktitle = {Runtime Verification},
  year = {2027},
  pages = {19--29},
  doi = {10.1007/978-3-032-41160-0_2}
}

For citation metadata, see CITATION.cff.

License

This project is distributed under the INTO-CPS Association Public License (ICAPL) with GPL v3 as a supported subsidiary mode. See LICENSE for the full terms and ICA-USAGE-MODE.txt for the selected usage mode in this distribution.