Signal Temporal Logic Monitoring

Description

Signal temporal logic (STL) monitoring checks the signals a system produces over time, such as speeds, distances, positions or a model's outputs, against safety requirements written in signal temporal logic, a formal language for stating how real-valued signals must behave over time intervals (for example, 'whenever the gap to the vehicle ahead falls below 10 m, speed drops below 5 m/s within 2 s'). Each requirement is built from comparisons of signals with thresholds, joined by logical operators and by timed operators such as 'always within [a, b]', 'eventually within [a, b]' and 'until'. For each trace the monitor computes a robustness value, a margin to the requirement rather than robustness to adversarial inputs: its sign says whether the requirement is met (positive) or violated (negative), and its size is a tolerance: any signal whose values stay closer than that to the observed ones at every instant gets the same verdict. Monitors run offline on logged or simulated traces, or online on live signals, where a requirement that looks ahead in time can be decided only once enough of the signal has arrived. RTAMT, the named tool, is an open-source Python library with an optional C++ back-end that builds such monitors from a written specification and connects to ROS and MATLAB/Simulink; its online monitors accept only requirements whose future time windows are bounded and give each verdict after a delay equal to the requirement's time horizon, and it reports the robustness value but does not act on it, so stopping or correcting the system is left to a separate safeguard.

Example Use Cases

Safety

A team developing an adaptive cruise controller with a learned speed policy writes its requirements in STL, for example that the time gap to the vehicle ahead never stays below one second for longer than two seconds, and attaches an RTAMT monitor to every drive in an urban driving simulator. The robustness values show which controller settings meet each requirement and by what margin, and drives with negative values become regression scenarios.

A hospital's service robot, which uses learned perception to find people, fetches supplies along corridors. The integrator monitors live ROS topics against a system requirement (always at least 0.5 m from any detected person) and against one requirement per subsystem, such as the planner reaching its next waypoint in time. When a subsystem requirement fails shortly before the system one, the logged verdicts show where the fault began.

A drone-delivery operator checks each day's flight logs from its learned landing controller against a requirement that, in the last ten seconds before touchdown, descent rate stays below 1 m/s and the drone stays within 0.5 m of the pad centre. It reports the smallest robustness value across all landings to its safety manager and investigates any landing whose value is negative.

Limitations

The monitor checks the requirement as written, not as intended. Writing correct STL needs fluency in the logic and in the system: a wrong threshold, a time window that is too short or a misplaced operator yields confident positive margins for behaviour the engineers would call unsafe, and nothing in the monitor reveals the mistake. Specifications need the same review as the requirements they encode.
Online monitoring judges a requirement from a partial trace. RTAMT's online monitors take only requirements whose future time windows are bounded, and give each verdict after a delay equal to the requirement's horizon: a check that something happens within five seconds is decided five seconds later, which may be too late to act on in a fast system. Monitors that track a narrowing range of possible robustness values can flag some violations sooner, but stay undecided until the data settles it.
A robustness value is measured in the units of the signals in the requirement, so a margin of 0.4 means 0.4 metres in one requirement and 0.4 degrees in another. Values cannot be compared across requirements, and when one requirement combines signals of different scales its value is set by whichever margin is numerically smallest, which depends on the units chosen unless the signals are normalised first.
Monitoring reports on the traces it sees. A clean record over many hours shows that those runs met the requirement, not that every possible run will, and a violation is reported when it happens, not before, unless a separate predictor of future signals is added. To protect the system, the verdict has to drive a safeguard such as a fallback controller, which the monitor does not provide.
The verdict is only as good as the signals. If a learned perception component misjudges the distance to a person, the monitor computes a confident margin from the wrong distance; independent sensors or ground truth are needed to check the perception itself. Discrete-time monitors see only the samples taken, so a brief violation between samples can go unseen, and the ROS integration assumes messages arrive at a known, regular rate.

Resources

Research Papers

Monitoring Temporal Properties of Continuous Signals

Oded Maler and Dejan Nickovic•Jan 1, 2004

Robustness of temporal logic specifications for continuous-time signals

Georgios E. Fainekos and George J. Pappas•Sep 1, 2009

RTAMT – Runtime Robustness Monitors with Application to CPS and Robotics

Tomoya Yamaguchi, Bardh Hoxha, and Dejan Ničković•Oct 5, 2023

Software Packages

RTAMT: specification-based real-time monitoring library for Signal Temporal Logic

Specification-based real-time monitoring library. Contribute to nickovic/rtamt development by creating an account on GitHub.

Tutorials

Specification-Based Monitoring of Cyber-Physical Systems: A Survey on Theory, Tools and Applications

Ezio Bartocci et al.•Jan 1, 2018

Related Techniques

Name	Description	Assurance Goals
Runtime Monitoring and Circuit Breakers	Runtime monitoring and circuit breakers observe a deployed AI service and restrict model calls when configured signals breach specified limits. In the closed state, requests pass through and recent failures are counted, while an open breaker rejects requests or provides a configured fallback, such as a cached answer, a simpler model, a rule-based default or referral to a person. After a waiting period, the half-open state permits a few trial calls and closes again only if they succeed. Model-related triggers can include immediately available signals such as input-drift scores (how far incoming data has moved from the training data) or low prediction confidence, since accuracy usually needs later outcome labels. Logs record state changes and triggering signals, supporting review of why the service was restricted without guaranteeing that the fallback is safe.	General Reliability Safety Transparency
API Usage Pattern Monitoring	API usage pattern monitoring examines how each account uses a deployed model's API, to catch misuse that no single request reveals. The monitor keeps a running record per account and compares it with a baseline of normal use, raising an alert when the account departs from it. Published detectors for model theft show two ways to do this: one tests whether the distances between an account's successive queries follow the bell-shaped pattern that ordinary use produces, and another estimates how much of the model's behaviour the account's queries and responses would let someone rebuild. Providers also score how often an account triggers content filters or repeats jailbreak attempts, and send high scores for review. The output is a log of alerts and the actions taken, which gives a dated record of how the API was used compared with the uses it was approved for.	Security Safety Transparency
Scenario-Based Simulation Testing	Scenario-based simulation testing checks an automated system, most often an automated driving system, by running it through a planned set of situations in a simulator and judging each run against criteria fixed in advance. Scenarios are written at three levels of detail: a functional scenario describes a situation in words (a car cuts in ahead on a motorway), a logical scenario turns it into parameters with ranges (speeds, gaps, road friction), and a concrete scenario fixes one value for every parameter so that the run can be reproduced exactly. Functional scenarios are derived from hazard analysis and from the operational design domain (the conditions the system is designed to work in), and concrete scenarios are sampled from the logical ranges, either to cover the whole range or to seek out rare, critical combinations, or are reconstructed from recorded incidents. Each concrete scenario is executed with the system under test in the loop, and pass or fail is decided against its expected behaviour, such as no collision, or by criticality measures such as time-to-collision, giving a record of which situations the system handles and which it does not. ISO 34502 gives a scenario-based safety evaluation framework of this kind for automated driving systems on limited-access highways.	Safety