💻 computer science

mstlo: Efficient Online Monitoring of Signal Temporal Logic

This paper introduces mstlo, a high-performance Rust library with Python bindings that enables efficient online monitoring of Signal Temporal Logic through a unified interface, an incremental dynamic programming algorithm with caching, and an embedded domain-specific language, demonstrating significant scalability improvements over existing tools.

Original authors: Andreas Kaag Thomsen, Niels Viggo Stark Madsen, Valdemar Tang Evans, Thomas David Wright, Lukas Esterle, Peter Gorm Larsen

Published 2026-05-27

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Andreas Kaag Thomsen, Niels Viggo Stark Madsen, Valdemar Tang Evans, Thomas David Wright, Lukas Esterle, Peter Gorm Larsen

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are the safety inspector for a high-speed train. Your job is to watch the speedometer, temperature gauges, and pressure valves in real-time. You have a rulebook (the "Signal Temporal Logic" or STL) that says things like: "If the temperature goes above 100 degrees, it must drop back below 90 within 5 minutes."

The problem with traditional safety inspectors is that they often wait until the entire 5 minutes are up before they can say, "Okay, that rule was followed," or "Oh no, it failed!" By the time they speak, the train might have already crashed.

Enter mstlo (pronounced "mistletoe").

Think of mstlo as a super-fast, super-smart digital inspector built with the programming language Rust (known for being incredibly fast and safe) and wrapped in a friendly Python coat so anyone can use it. Here is how it works, using simple analogies:

1. The "Early Verdict" Superpower

Most inspectors wait for the whole story to unfold. mstlo is different. It uses a trick called "short-circuiting."

The Analogy: Imagine a rule that says, "You must not touch the fire." If you see someone reach out and touch the fire, you don't wait to see if they pull their hand back in 5 seconds. You scream "VIOLATION!" immediately.
In the Paper: This is called Eager Qualitative semantics. If a rule is broken, mstlo stops waiting and gives you the answer instantly, saving precious time.

2. The "Fuzzy Interval" Crystal Ball

Sometimes, you don't know the final answer yet, but you want to know how close you are to disaster.

The Analogy: Instead of a simple "Pass/Fail," mstlo gives you a range, like a weather forecast saying, "The temperature will be between 80 and 120 degrees."
- If the lowest possible number in that range is still safe, you know you're good.
- If the highest possible number is dangerous, you know you're in trouble.
- If the range is mixed, it keeps watching.
In the Paper: This is called RoSI (Robust Satisfaction Intervals). It calculates a "safety margin" that shrinks as more data comes in, giving you a nuanced view of how well the system is doing without waiting for the final moment.

3. The "Sliding Window" Trick (The Secret Sauce)

To check rules like "Stay under the speed limit for the next 10 minutes," a slow computer has to look back at the last 10 minutes of data every single second. That's like re-reading the last 10 pages of a book every time you turn a new page.

The Analogy: mstlo uses a clever math trick (Lemire's algorithm) that acts like a sliding window. Instead of re-reading everything, it just updates the "highest" and "lowest" values as new data slides in and old data slides out. It's like a conveyor belt where you only check the new item arriving, not the whole pile.
In the Paper: This makes the tool incredibly fast, especially for rules that look far into the future (large "temporal depth").

4. The "Magic Spell" (The DSL)

Writing complex logic rules in code can be messy and prone to typos.

The Analogy: mstlo gives you a Domain-Specific Language (DSL). Think of this as a special "magic spell" syntax. You can write a rule like G[0, 5] (temp < $MAX_TEMP) (meaning "Always, for 5 seconds, temp must be less than MAX_TEMP").
The Benefit: If you make a typo in your spell, the computer catches it before you even run the train (static checking). It also lets you swap out variables (like changing the temperature limit) without rewriting the whole spell.

5. How Fast is it?

The authors tested mstlo against the best existing tools (like a tool called RTAMT).

The Result: mstlo is significantly faster. For simple rules, it's about 10 to 13 times faster. For complex rules with deep time windows, it can be 39 times faster.
Why? Because it's written in Rust (a very efficient language) and uses the smart "sliding window" math tricks mentioned above, whereas older tools often re-calculate everything from scratch or rely on slower languages.

Summary

mstlo is a new, high-performance tool that lets engineers watch complex systems in real-time. It doesn't just wait for the end of the story to tell you if you failed; it spots problems the instant they happen, gives you a "safety score" while you wait, and does all of this at lightning speed using smart math tricks. It's available for both Rust developers and Python users, making it easy to plug into modern engineering projects.

Technical Summary: mstlo – Efficient Online Monitoring of Signal Temporal Logic

1. Problem Statement

The increasing deployment of Cyber-Physical Systems (CPS) necessitates robust methods for ensuring correctness during operation. Runtime Verification (RV) addresses this by monitoring system behavior in real-time against formally specified properties. Signal Temporal Logic (STL) is a standard language for specifying timing constraints and safety requirements over real-valued continuous-time signals.

However, existing online monitoring tools face significant challenges:

Performance Constraints: Monitors must be highly efficient to minimize latency and ensure the verification process does not lag behind the system. Naive approaches that re-evaluate formulas from scratch at every time step scale poorly with formula complexity and signal length.
Semantic Limitations: Most tools restrict users to a single evaluation strategy (e.g., only delayed quantitative semantics), limiting the ability to trade off between verdict expressiveness, latency, and performance.
Usability and Integration: There is a lack of tools that offer a unified interface for multiple STL semantics while providing an embedded Domain-Specific Language (DSL) for static syntax checking and easy integration into modern ecosystems like Rust and Python.

2. Methodology

The authors present mstlo (mistletoe), a high-performance library implemented in Rust with Python bindings, designed for efficient online monitoring of STL.

Core Algorithmic Approach

Incremental Monitoring: Instead of re-evaluating the entire formula at every time step, mstlo employs a bottom-up dynamic programming approach. The specification is represented as an Abstract Syntax Tree (AST) where each operator maintains a cache of intermediate results from its child operators.
Optimized Temporal Operators: For globally ( $\square$ ) and eventually ( $\diamond$ ) operators, which function as sliding window minimum and maximum computations, the implementation incorporates a version of Lemire's algorithm. This optimization significantly reduces memory footprint and computational time for non-RoSI semantics.
Unified Semantics Interface: The library supports four distinct semantic definitions via a single generic monitoring core using Rust traits for zero-cost static dispatch:
1. Delayed Qualitative: Standard Boolean satisfaction requiring full signal resolution up to temporal depth.
2. Delayed Quantitative: Standard robustness semantics computing a real-valued score.
3. Eager Qualitative: Leverages monotonicity to emit early Boolean verdicts (short-circuiting) over partial traces (e.g., immediately returning false upon the first violation of a $\square$ property).
4. Robust Satisfaction Intervals (RoSI): Computes an interval $[\rho_{min}, \rho_{max}]$ enclosing all possible future robustness values for partial traces, converging to a single value once the full horizon is observed.

Implementation Features

Embedded DSL: mstlo provides a DSL available as a compile-time procedural macro (stl!) for Rust and a runtime parser. This supports static syntax checking, parametrized formulas (via symbolic variables prefixed with $), and syntactic sugar for common patterns.
Builder Pattern: Monitors are instantiated using a builder pattern to configure formulas, semantics, algorithmic modes (Naive vs. Incremental), variable contexts, and synchronization strategies (e.g., handling asynchronous signal interpolation).
Cross-Language Support: The core engine is written in Rust, with Python bindings (mstlo-python) wrapping the engine to facilitate adoption in the Python ecosystem and interactive workflows (e.g., Jupyter Notebooks).

3. Key Contributions

Unified Framework: The first dedicated tool for online monitoring supporting multiple STL semantics (Delayed Qualitative/Quantitative, Eager Qualitative, and RoSI) within a single architecture.
High-Performance Algorithm: An incremental monitoring algorithm utilizing per-operator caching and Lemire's sliding-window optimization, achieving scalability for formulas with large temporal depths.
Developer Experience: An embedded DSL with static syntax checking in Rust and a runtime parser, alongside Python bindings for broader accessibility.
Reproducible Benchmarking: A comprehensive benchmark suite evaluating performance across different semantics, formula structures, and input signals.

4. Experimental Results

Benchmarks were conducted on an Apple MacBook M4 Pro using a chirp wave signal sampled at 1 Hz over 20,000 samples. Three formulas ( $\phi_1, \phi_2, \phi_3$ ) with varying temporal depths and nesting were evaluated.

Scalability:
- For Delayed and Eager Qualitative semantics, execution time for the $\square$ operator remained constant regardless of the temporal upper bound $b$ due to Lemire's optimization.
- Execution time for the $U$ (Until) operator scaled linearly with $b$ , as it does not benefit from the same optimization.
- RoSI semantics showed linear scaling for $\square$ and quadratic scaling for $U$ , reflecting the higher computational cost of maintaining intervals.
Performance Comparison:
- mstlo (Rust) demonstrated significantly lower execution times compared to RTAMT (a leading Python-based tool with a C++ backend).
- For simple formulas ( $\phi_1$ ), mstlo-python was 10–13 times faster than RTAMT.
- For complex nested formulas ( $\phi_3$ ), mstlo-python was approximately 39 times faster.
- The performance gap is attributed to mstlo's algorithmic optimizations (caching) and shallow Python bindings compared to RTAMT's heavier reliance on Python.
Overhead: The Python bindings introduced only a small overhead (1–1.7 $\times$ ) compared to the native Rust implementation.

5. Significance and Claims

The paper claims that mstlo advances the state of the art in STL monitoring by:

Bridging the Gap: Providing an easy-to-use, dedicated online framework for both Rust and Python that supports multiple evaluation semantics, addressing the scarcity of tools optimized for online STL monitoring.
Architectural Advancement: Introducing architectural improvements tailored for high-performance online monitoring, specifically the combination of incremental algorithms with Lemire's optimization.
Usability: Enhancing usability through an embedded DSL that offers static syntax checking and parameterization, reducing the barrier to entry for specifying complex temporal properties.
Practical Application: The tool has already been successfully utilized in an educational context ("Engineering Digital Twins" course) to teach Runtime Verification in practical settings.

The authors note that future work includes extending the implementation to embedded systems platforms, where memory and computational constraints impose additional requirements.