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 applications. The Python bindings are published as mstlo-python.

mstlo

About

Cyber-Physical Systems (CPSs) increasingly rely on real-time fault detection and runtime monitoring to ensure safe operation. mstlo provides a unified monitoring interface that addresses the stringent performance requirements of these systems. Key features include:

Embedded DSL: A macro-based DSL (stl!) allows specifications to be embedded and syntax-checked directly at compile time in Rust.
Unified Semantics Interface: Supports multiple online evaluation modes (Qualitative, Quantitative, Eager, and RoSI) in a single framework.
Python Bindings: Exposed via the mstlo-python package (import name: mstlo_python) to enable interactive workflows in environments like Jupyter Notebooks.
High Performance: Benchmarks demonstrate throughput exceeding existing state-of-the-art tools.

Published package pages:

Rust crate: crates.io/crates/mstlo
Python package: pypi.org/project/mstlo-python
Rust API docs: docs.rs/mstlo
Python docs: INTO-CPS-Association.github.io/mstlo

Installation

Rust

Add mstlo to your Cargo.toml:

[dependencies]
mstlo = "0.1.0"

Python

Install the Python bindings via pip:

pip install mstlo-python

Usage

Rust Usage

For more examples, see the mstlo/examples directory. The following snippet demonstrates how to create a monitor for the STL formula $\Box_{[0, 2]}(x > 5)$ using the embedded DSL and process incoming signal data.

mstlo utilizes the Builder pattern to configure the monitor's formula, semantics, and algorithm before processing the data stream.

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

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, robustness value is in interval (-inf, 2.0)
    let out2 = monitor.update(&step!("x", 4.0, 1s));
    println!("{:?}", out2.verdicts());
    // Output after second update: [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
}

Python Usage

For more Python examples, see the mstlo-python/examples directory. The Python API wraps the core Rust engine, offering comparable performance via an intuitive Pythonic interface.

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 formatted verdicts or extract structured data
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

Theory

Signal Temporal Logic (STL)

Signal Temporal Logic (STL) [3] is a formalism for specifying properties of real-valued signals that evolve over time, providing a compact language to describe the desired behaviors of dynamic systems. STL evaluates properties over signals, which are defined as functions mapping a time domain (such as nonnegative real numbers, $\mathbb{R}_{\ge0}$) to a value domain.

mstlo focuses on bounded STL, meaning all temporal operators are constrained by finite time intervals of the form $[a, b]$, where $0 \le a < t$.

The core syntax of STL is built from a minimal set of primitive operators:

True ($\top$): The Boolean constant True.
Atomic Predicates ($\mu(x) < c$): Evaluates to True if the function over the signal is less than a constant $c$.
Negation ($\neg\phi$): The logical NOT of a formula.
Conjunction ($\phi \wedge \psi$): The logical AND of two formulas.
Until ($\phi \mathcal{U}_{[a,b]} \psi$): States that $\phi$ must hold continuously until $\psi$ becomes true within the time interval $[a, b]$.

From these primitives, the library derives other highly useful operators to simplify specifications:

Disjunction (OR): $\phi \vee \psi$
Implication: $\phi \rightarrow \psi$
Eventually: $\diamondsuit_{[a,b]}\phi$
Globally: $\Box_{[a,b]}\phi$

Evaluation Semantics

See also semantics-comparison.ipynb for an interactive demonstration of the different semantics.

An online monitor observes a system's behavior incrementally as discrete samples arrive. mstlo provides a unified interface supporting four distinct monitoring semantics, allowing users to trade off between expressiveness and verdict latency:

Delayed Qualitative

The standard Boolean semantics of STL [3], where the monitor emits a strict true/false verdict only after observing enough of the signal (the temporal depth) to conclusively determine satisfaction or violation. Formally, the semantics are defined as follows:

$$ ⟦ \cdot ⟧ : \mathrm{Formula} \to (\mathrm{Signal} \times \mathbb{T}) \to \mathbb{B} $$

$$ ⟦ \mu ⟧(s,t) = (s(t) \models \mu) $$

$$ ⟦ \neg \varphi ⟧ (s,t) = \neg ⟦ \varphi ⟧ (s,t) $$

$$ ⟦ \varphi_1 \land \varphi_2 ⟧(s,t) = ⟦ \varphi_1 ⟧(s,t) \land ⟦ \varphi_2 ⟧(s,t) $$

$$ ⟦ \varphi_1 \lor \varphi_2 ⟧(s,t) = ⟦ \varphi_1 ⟧(s,t) \lor ⟦ \varphi_2 ⟧(s,t) $$

$$ ⟦ \mathbf{G}_I \varphi ⟧(s,t) = \forall t' \in t + I.\ ⟦ \varphi ⟧(s,t') $$

$$ ⟦ \mathbf{F}_I \varphi ⟧(s,t) = \exists t' \in t + I.\ ⟦ \varphi ⟧(s,t') $$

$$ ⟦ \varphi \ \mathbf{U}_I\ \psi ⟧(s,t) = \exists t' \in t + I.\ (⟦ \psi ⟧(s,t') \land \forall t'' \in [t,t'].\ ⟦ \varphi ⟧(s,t'')) $$

Delayed Quantitative

The typical quantitative semantics of STL, as introduced by Donzé and Maler [1], computes a real-valued robustness score indicating the precise degree of satisfaction or violation. Similar to the qualitative mode, it requires full signal availability up to the temporal depth. It is defined as follows:

$$ \rho : \mathrm{Formula} \to (\mathrm{Signal} \times \mathbb{T}) \to \mathbb{R} $$

$$ \rho(s_t, \mu_c) = c - \mu(x_t) $$

$$ \rho(s_t, \neg\phi) = -\rho(s_t, \phi) $$

$$ \rho(s_t, \phi \wedge \psi) = \min\left(\rho(s_t, \phi), \rho(s_t, \psi)\right)
$$

$$ \rho(s_t, \phi \vee \psi) = \max\left(\rho(s_t, \phi), \rho(s_t, \psi)\right)
$$

$$ \rho(s_t, \phi \rightarrow \psi) = \max\left(-\rho(s_t, \phi), \rho(s_t, \psi)\right) $$

$$ \rho(s_t, \Diamond_{[a,b]}\phi) = \max_{t' \in t+[a,b]} \rho(s_{t'}, \phi) $$

$$ \rho(s_t, \Box_{[a,b]}\phi) = \min_{t' \in t+[a,b]} \rho(s_{t'}, \phi) $$

$$ \rho(s_t, \varphi \ \mathbf{U}I\ \psi) = \max{t' \in t+[a,b]} \left(\min\left(\rho(s_{t'},\psi), \max_{t'' \in [t, t']} \rho(s_{t''},\phi)\right)\right) $$

Robust Satisfaction Intervals (RoSI)

As introduced by Deshmukh et al. [3], this semantics provides quantitative reasoning over partial traces. Instead of a single robustness value, the monitor computes an interval $[\rho_{min}, \rho_{max}]$ that encloses all possible future robustness values. A formula is definitively satisfied when $\rho_{min} > 0$ and definitively violated when $\rho_{max} < 0$. Formally, the semantics are defined as:

$$ [\rho] : \mathrm{Formula} \to (\mathrm{Signal} \times \mathbb{T}) \to \mathcal{I}(\mathbb{R}) $$

$$ [\rho](x_{[0,i]}, \tau, \mu_c) = \begin{cases} [\mu(x_{[0,i]}(\tau)), \mu(x_{[0,i]}(\tau))] \text{if } \tau \in [t_0, t_i] \ [-\infty, \infty] \text{otherwise} \end{cases} $$

$$ [\rho](x_{[0,i]}, \tau, \neg\phi) = -[\rho](x_{[0,i]}, \tau, \phi) $$

$$ [\rho](x_{[0,i]}, \tau, \phi \wedge \psi) = \min([\rho](x_{[0,i]}, \tau, \phi), [\rho](x_{[0,i]}, \tau, \psi))
$$

$$ [\rho](x_{[0,i]}, \tau, \phi \vee \psi) = \max([\rho](x_{[0,i]}, \tau, \phi), [\rho](x_{[0,i]}, \tau, \psi))
$$

$$ [\rho](x_{[0,i]}, \tau, \phi \rightarrow \psi) = \max(-[\rho](x_{[0,i]}, \tau, \phi), [\rho](x_{[0,i]}, \tau, \psi)) $$

$$ [\rho](x_{[0,i]}, \tau, \Diamond_{[a,b]}\phi) = \sup_{t' \in \tau + [a,b]} \left([\rho](x_{[0,i]}, t', \phi)\right) $$

$$ [\rho](x_{[0,i]}, \tau, \Box_{[a,b]}\phi) = \inf_{t' \in \tau + [a,b]} \left([\rho](x_{[0,i]}, t', \phi)\right) $$

$$ [\rho](x_{[0,i]}, \tau, \varphi \ \mathbf{U}I\ \psi ) = \sup{t' \in \tau + [a,b]} \min\left( [\rho](x_{[0,i]}, t', \psi), \inf_{t'' \in [\tau, t']} [\rho](x_{[0,i]}, t'', \phi) \right) $$

Where $x_{[0,i]}$ is the signal prefix observed up to time $t_i$, $\tau$ is the timestamp of interest, and $\mathcal{I}(\mathbb{R})$ denotes the set of all intervals over the reals.

Eager Qualitative

Leverages the monotonicity in Boolean and temporal logic to emit early verdicts over partial traces. For example, a violation of a "globally" ($\mathbf{G}$) property immediately yields a false verdict without waiting for the full interval to elapse, and satisfaction of an "eventually" ($\mathbf{F}$) property yields a true verdict as soon as the condition is met. This semantics agrees with RoSI in terms of early verdicts but does not provide quantitative information, and is thus significantly more efficient to compute. The semantics alter the delayed qualitative semantics to work over partial traces, by introducing a set of short-circuiting rules.

Implementation

To compute these semantics efficiently, mstlo uses a bottom-up dynamic programming approach. For sliding window operations (like eventually and globally), the library incorporates Lemire's algorithm to aggressively reduce cache footprints and computation time.

Building from Source

Prerequisites

Rust (stable toolchain)
Python 3.9+ and maturin (for Python bindings only)

Rust Crate

git clone https://github.com/INTO-CPS-Association/mstlo.git
cd mstlo/mstlo
cargo build

Run the test suite:

cargo test

Run the included examples:

cargo run --example intro_example
cargo run --example simple_example
cargo run --example variables_example

Python Bindings

cd mstlo-python
pip install maturin
maturin develop

Run the Python tests:

pip install pytest
pytest

References

[1] A. Donzé and O. Maler, “Robust Satisfaction of Temporal Logic over Real-Valued Signals,” in Formal Modeling and Analysis of Timed Systems, K. Chatterjee and T. A. Henzinger, Eds., Berlin, Heidelberg: Springer, 2010, pp. 92–106. doi: 10.1007/978-3-642-15297-9_9.

[2] J. V. Deshmukh, A. Donzé, S. Ghosh, X. Jin, G. Juniwal, and S. A. Seshia, “Robust online monitoring of signal temporal logic,” Form Methods Syst Des, vol. 51, no. 1, pp. 5–30, Aug. 2017, doi: 10.1007/s10703-017-0286-7.

[3] O. Maler and D. Nickovic, “Monitoring Temporal Properties of Continuous Signals,” in Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Y. Lakhnech and S. Yovine, Eds., Berlin, Heidelberg: Springer, 2004, pp. 152–166. doi: 10.1007/978-3-540-30206-3_12.

[4] D. Lemire, “Streaming maximum-minimum filter using no more than three comparisons per element,” Nordic J. of Computing, vol. 13, no. 4, pp. 328–339, Dec. 2006.

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.

mstlo 0.1.1