1 Introduction↩︎

The growing deployment of Cyber-Physical Systems (CPSs) motivates the use of methods for ensuring correctness during operation [1]. One widely adopted approach is Runtime Verification (RV), in which a monitor observes the system’s behavior in real time and checks it against formally specified properties [2]. Among the specification languages used in this context, Signal Temporal Logic (STL) [3] is widely used for CPSs, enabling precise specification of timing constraints, safety requirements, and performance bounds over real-valued continuous-time signals. STL admits both qualitative and quantitative semantics, along with offline and online monitoring algorithms [3], [4]. In online monitoring, an important goal is to produce a verdict as early as possible, without waiting for the full temporal depth of the specification to elapse. This capability is essential for real-time fault detection but imposes stringent performance requirements: the monitor must be highly efficient to minimize latency and ensure the verification process does not lag behind the system itself.

In this paper, we present mstlo, a high-performance RV library implemented in Rust. Our tool provides a user-friendly interface for writing STL formulas and building monitors, while delivering the efficiency and performance required for production deployment. mstlo is the first dedicated tool for online monitoring of multiple STL semantics, which includes delayed verdicts, so-called Robust Satisfaction Intervals (RoSIs) as well as Boolean early verdicts. Our tool provides the following key features:

• Unified Semantics Interface: We provide a unified framework supporting multiple online evaluation semantics via efficient stateful streaming algorithms.

• Embedded Domain-Specific Language (DSL): We introduce a Rust macro-based DSL integrating STL specifications directly into source code, with parametrized formulas, syntactic sugar, and static syntax checking via procedural macros¹.

• Efficiency and Benchmarking: We demonstrate that our incremental algorithm is scalable and achieves high throughput exceeding state-of-the-art tools, and provide a reproducible benchmark suite for hardware-specific performance evaluation.

• Open-source Rust crate with Python bindings: Our library is available as an open-source Rust crate, ensuring accessibility and ease of integration. Additionally, we provide Python bindings to facilitate adoption within the widely-used Python ecosystem.

The source code for mstlo is available at GitHub², along with documentation, installation instructions, examples and comprehensive tests. mstlo has also been successfully used in a teaching context in the course “Engineering Digital Twins” [5] where it has been used to teach students about how to use RV for monitoring in a practical setting³.

2 Preliminaries↩︎

In the context of RV, we focus specifically on online monitoring, where the signal is observed incrementally as a stream of samples rather than as a complete trace available a priori. Additionally, batch processing is also supported, e.g., for post-hoc analysis of logged data.

Signal Temporal Logic

An STL formula \(\phi\) is defined recursively by the grammar: \(\phi ::= \top \mid \mu(x)<c \mid \neg\phi \mid \phi\wedge\psi \mid \phi \mathop{\mathcal{U}_{[a, b]}} \psi\), where \(\mu\) is an atomic predicate over the signal \(x\), \(\top\) denotes Boolean truth, and \(\mathcal{U}_{[a,b]}\) is the time-bounded until operator, requiring \(\psi\) to hold at some time within \([a,b]\) while \(\phi\) holds continuously beforehand. Standard derived operators include disjunction, implication, and the temporal operators eventually (\(\Diamond\)) and globally (\(\Box\))⁴. The temporal depth \(H(\phi)\) [6] defines the maximum future horizon required to evaluate a formula, which dictates the worst-case buffering requirements for a monitor using delayed semantics. The expressiveness of STL allows for the compact specification of complex temporal properties, such as “within the next 100 minutes, whenever the temperature \(T\) exceeds 100 degrees, it must return below 90 degrees within 5 minutes” and can be expressed as: \(\Box_{[0,100]}\left((T > 100) \rightarrow \Diamond_{[0,5]} (T < 90)\right).\)

Supported STL Semantics

Existing tools often restrict users to a single evaluation strategy. mstlo, however, implements a unified interface for four distinct semantic definitions, allowing users to trade off between verdict expressiveness, verdict latency and performance:

• Delayed Qualitative: The standard Boolean satisfaction \((s,t) \models \phi\) [3]. This requires the signal to be fully resolved up to the temporal depth \(H(\phi)\) before a verdict is emitted.

• Delayed Quantitative: The standard robustness semantics \(\rho(s_t, \phi)\) [7], which computes a real-valued score indicating the degree of satisfaction or violation. Similar to delayed qualitative semantics, this requires full signal availability up to \(H(\phi)\).

• Eager Qualitative: Inspired by [8], this semantics leverages monotonicity in Boolean and temporal logic to emit early verdicts over partial traces via short-circuiting. For example, \(\Box_{[0,10]} \phi\) yields \(\bot\) (false) immediately upon the first violation of \(\phi\), without waiting for the full interval to elapse.

• RoSI: The RoSI semantics \([\rho](\varphi,x_ {[0,i]},t)\) [4] support quantitative reasoning over partial traces. Instead of a single robustness value \(\rho\), the monitor computes an interval \([\rho_{\text{min}}, \rho_{\text{max}}]\) enclosing all possible future robustness values. A formula is definitively satisfied when \(\rho_{\text{min}} > 0\) and violated when \(\rho_{\text{max}} < 0\). The interval is updated incrementally as new signal samples arrive and converges to \(\rho(s_t, \phi)\) once the full horizon is observed.

3 Efficient Online Monitoring Algorithms↩︎

A naive approach to STL monitoring involves re-evaluating the entire formula from scratch at every time step, a process that scales poorly with formula complexity and signal length. To address this, mstlo implements an incremental monitoring algorithm based on a bottom-up dynamic programming approach, enabling efficient reuse of intermediate results across timesteps. In our implementation, the specification is internally represented as an Abstract Syntax Tree (AST), in which each operator maintains its own cache of intermediate results from its child operators. While this provides a significant performance boost over the naive method, temporal operators can still require intensive searches over large caches to determine a verdict. To mitigate this for globally (\(\Box\)) and eventually (\(\Diamond\)) operators—which are essentially sliding window minimum and maximum computations—we incorporate a version of Lemire’s algorithm [9]. This optimization significantly reduces both the memory footprint of the caches and the computational time required to emit a verdict at each step. It is most effective for non-RoSI semantics; since RoSI intervals frequently overlap, particularly in nested formulas, the optimization applies less frequently and still requires a search over the entire cache, yielding comparatively modest gains.

4 The mstlo Tool↩︎

mstlo is built around a single generic monitoring core that uses Rust traits to support multiple semantics with zero-cost static dispatch. In the following, we describe the key features of the tool.

Monitoring Modes↩︎

mstlo supports the four monitoring modes DelayedQuantitative, DelayedQualitative, EagerQualitative, and Rosi (2). These modes are implemented via the Semantics configuration, which determines the type of the verification output. Additionally, the monitor can operate in two algorithmic modes: Naive, which re-evaluates the formula at every step, and Incremental (default), which optimizes performance by only updating the necessary state (3). The monitor will output a verdict for each timestep input into the system.

DSL↩︎

mstlo provides an intuitive DSL available both as a compile-time procedural macro (stl!) for Rust applications and as a runtime parser. The macro-based approach allows for benefits such as static syntax checking with expressive error messages; while the runtime parser supports loading configurations dynamically at runtime and also enables the DSL for Python bindings.

The DSL supports standard STL syntax as well as syntactic sugar for common patterns with both shorthand and symbolic notation (e.g. G/globally and &&/and). It also supports symbolic variables (prefixed with $) allowing for parameterized specifications where thresholds can be updated at runtime. Nested specifications are also supported, enabling modular and reusable formula definitions.

let phi1 = stl!(G[0, 5] (temp < $MAX_TEMP));
let phi2 = stl!(pressure > 10.0 -> F[0, 2] valve_open == 1.0);
let phi = stl!(phi1 and phi2);

Building a Monitor↩︎

mstlo utilizes the Builder pattern [10], allowing users to configure the formula, semantics, algorithm, variable context, and synchronization strategy (i.e., how signal data is interpolated when signals arrive asynchronously) before instantiation. Defaults are provided for all options.

let vars = Variables::new(); // Define variables context
vars.set("MAX_TEMP", 120.0);
let mut monitor = StlMonitor::builder() // Build the monitor
    .formula(phi)
    .variables(vars)
    .semantics(Rosi)
    .synchronization_strategy(ZeroOrderHold)
    .build()
    .expect("Failed to build monitor");

Updating the Monitor

Once built, the monitor accepts a stream of data points via the update method, which takes a Step containing the signal name, value, and timestamp, and returns a MonitorOutput with any new verdicts, as shown in [lst:monitor_update], which prints t=0s: RobustnessInterval(-inf, -5.5) for the given inputs. A verdict can only be produced for a given time step once all relevant signals have been updated and the monitor has sufficient information to evaluate the formula according to its semantics.

monitor.update(&step!("temp", 125.5, 0s));
monitor.update(&step!("pressure", 15.0, 0s));
let output = monitor.update(&step!("valve_open", 1.0, 0s));
println!("{}", output);

Batch updates are also supported, allowing users to feed multiple steps at once and retrieve all resulting verdicts in a single call.

Python Bindings↩︎

mstlo includes Python bindings exposed via the mstlo-python package, wrapping the core Rust engine with a Python API and enabling interactive workflows in environments like Jupyter Notebooks.

formula = mstlo.parse_formula("G[0, 10](x > 5)") # Parse from string
monitor = mstlo.Monitor(formula, semantics="Rosi")
output = monitor.update("x", 6.0, 0.5) # (signal_name, value, timestamp)
print(f"Verdicts: {output}")

5 Experimental Results↩︎

To evaluate mstlo, we conduct a series of benchmarks. Performance can vary significantly with the monitored formula (in terms of nesting and temporal depth), the chosen semantics, and the input signal (e.g., the signal’s frequency and its variation over time, as well as value trends relative to the formula). These benchmarks provide a representative performance overview showcasing differences across semantics and central algorithm optimizations.

The input signal is a chirp wave (i.e.a sinusoidal signal whose frequency decreases linearly over time) from \(f_0=10^{-1}\) Hz to \(f_1=10^{-4}\) Hz, producing values in \([-1, 1]\). We sample the signal at 1 Hz for a total of 20,000 samples, although the monitor is designed to handle variable, unknown sampling rates. Three formulas are evaluated: \[\begin{align} \varphi_1 & = (x < 0.5) \wedge (x > -0.5) \\ \varphi_2 & = \square_{[0,1000]}\bigl(x > 0.5 \to \Diamond_{[0,100]}(x < 0.0)\bigr) \\ \varphi_3 & = (x < 0.5) \mathop{\mathcal{U}_{[0, 1000]}} (x < 0.0) \end{align}\] as well as the parameterized temporal formulas \(\square_{[0,b]}\psi_1\), \(\Diamond_{[0,b]}\psi_1\), and \(\psi_1 \mathop{\mathcal{U}_{[0, b]}} \psi_2\) for each \(b \in \{1, 100, 200, \ldots, 5000\}\), where \(\psi_1 = (x > 0.0)\) and \(\psi_2 = (x < 0.0)\). These predicates ensure the signal crosses the threshold repeatedly, exercising both satisfaction and violation, while also preventing trivial short-circuiting, and ensuring balanced use of Lemire’s optimization. All benchmarks were conducted on an Apple MacBook M4 Pro (24 GB RAM), averaging over \(M = 50\) runs per formula.

Performance of mstlo

1 shows how execution time scales with the temporal upper bound \(b\). We show only the performance for \(\psi_1 \mathop{\mathcal{U}_{[0, b]}} \psi_2\) and \(\square_{[0,b]}\psi_1\) since \(\Diamond_{[0,b]}\psi_1\) performs similarly to \(\square_{[0,b]}\psi_1\). For delayed and eager semantics, performance is constant for \(\square_{[0,b]}\psi_1\) (due to Lemire’s optimization) and linear for \(\psi_1 \mathop{\mathcal{U}_{[0, b]}} \psi_2\), which does not benefit from it. Eager qualitative semantics consistently outperforms delayed semantics via short-circuiting. For RoSI, execution time scales linearly with \(b\) for \(\square_{[0,b]}\psi_1\) and quadratically for \(\psi_1 \mathop{\mathcal{U}_{[0, b]}} \psi_2\).

[tab:comparison] compares the performance across \(\varphi_1\), \(\varphi_2\), and \(\varphi_3\). The Python bindings introduce only a small overhead compared to Rust (about \(1{-}1.7\times\)). The results agree with the scaling trends observed in 1, with execution time increasing with temporal depth and temporal nesting, and the RoSI semantics being notably more expensive than the other semantics. Cache usage reflects formula structure and semantics. For \(\varphi_1\), which has no temporal operators, no caching is needed. For nested formuals (\(\varphi_2\)), qualitative semantics use minimal caching, while quantitative semantics require substantially more. RoSI incurs the highest cost, but behaves similarly to delayed quantitative semantics when nesting is absent. The cache usage is identical across semantics for \(\varphi_3\) since \(\mathcal{U}\) does not employ any cache optimization.

  3pt

6 Related Work & Comparison↩︎

RV has a rich history of ensuring system safety through dynamic analysis [11], [12]. Dedicated tools for online STL monitoring are, however, sparse. To our knowledge, the only existing tool optimized for online STL monitoring is the Python library RTAMT [6], which employs optimized, incremental update strategies for streaming data, though it currently only supports delayed quantitative semantics. In [tab:comparison], we compare against its discrete-time online monitor, which has an optimized C++ backend; like mstlo’s delayed quantitative semantics, it performs incremental robustness evaluation with a fixed delay of \(H(\varphi)\). For all formulas, mstlo-python is faster than RTAMT (Mann-Whitney U, two-sided, all \(p \ll 0.01\)), with per-sample means \(10{-}13 \times\) lower for \(\varphi_1,\varphi_2\) and \(39\times\) for \(\varphi_3\). This gap is not solely attributable to mstlo’s algorithmic approach; RTAMT’s heavier reliance on Python compared to mstlo’s shallow bindings likely contributes to the overhead. Also, RTAMT’s discrete-time monitor does not employ cache optimization and the temporal operators thus scales linearly (\(\Diamond\), \(\Box\)) or quadratically (\(\mathcal{U}\)) with their temporal depths. RTAMT’s dense-time online monitor, on the other hand, does implement cache optimization, but does not support the \(\mathcal{U}\) operator, and is written in pure Python, limiting its performance.

Beyond RTAMT, several tools address related use cases. The C++/MATLAB toolbox Breach [13] provides the foundation for STL monitoring and analysis and primarily targets falsification, model testing, and offline analysis. It includes an online module that computes RoSI, but this is designed around a fixed evaluation point rather than a sliding window; at each new time step the monitor re-evaluates over the full accumulated signal rather than updating incrementally, which limits its applicability to settings where the time horizon is known and fixed in advance. Within the Rust ecosystem, Banquo⁵ provides a STL parser and offline monitoring capabilities.

mstlo bridges these gaps by providing an easy-to-use dedicated online framework for both Rust and Python that supports multiple online evaluation semantics, and introduces architectural advancements tailored for high-performance online monitoring. Furthermore, mstlo provides a DSL with both a procedural macro for Rust as well as a runtime parser.

7 Conclusion↩︎

In this paper, we presented mstlo, a Rust-based library for efficient online STL monitoring. By combining multiple evaluation semantics into a unified framework with an incremental algorithm leveraging Lemire’s sliding-window optimization, implemented in Rust, mstlo advances both the performance and usability of STL monitoring over existing tools. The embedded DSL adds to this by providing an intuitive way to specify STL formulas, with benefits such as static syntax checking. Additionally, Python bindings ensure accessibility. Directions for future work include extending the implementation to embedded systems platforms, where memory and computational constraints impose additional requirements on the monitoring architecture.

Acknowledgements↩︎

This work was partially supported by the Grundfos Foundation under the project DT-CORE and by EU Horizon Europe project RoboSAPIENS under agreement number 101133807.

References↩︎