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.
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-pythonpackage (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
Add mstlo to your Cargo.toml:
[dependencies]
mstlo = "0.1.0"Install the Python bindings via pip:
pip install mstlo-pythonFor more examples, see the mstlo/examples directory.
The following snippet demonstrates how to create a monitor for the STL formula
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
}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 violationSignal 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,
mstlo focuses on bounded STL, meaning all temporal operators are constrained by finite time intervals of the form
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$
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:
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:
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:
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
Where
Leverages the monotonicity in Boolean and temporal logic to emit early verdicts over partial traces. For example, a violation of a "globally" (
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.
- Rust (stable toolchain)
- Python 3.9+ and maturin (for Python bindings only)
git clone https://github.com/INTO-CPS-Association/mstlo.git
cd mstlo/mstlo
cargo buildRun the test suite:
cargo testRun the included examples:
cargo run --example intro_example
cargo run --example simple_example
cargo run --example variables_examplecd mstlo-python
pip install maturin
maturin developRun the Python tests:
pip install pytest
pytest[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.
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.