We present a method and an interactive tool named LLMon that utilizes an LLM for synthesizing RV monitors from temporal or natural language (NL) specifications. Our focus is on allowing the flexibility of defining further temporal constructs on top of the standard ones; it helps to better customize the temporal formalism for expressing requirements originally given in NL. Our method allows the user to define new temporal operators through interaction with the tool. The LLM reframes the given descriptions of new operators, provided by the user in natural language, and synthesizes code for each alternative description. It performs analysis that compares the alternative generated codes, based on searching for traces with distinguishing verdicts. It then generates verbal descriptions that help the user to select the correct semantic interpretation. The tool can be used to synthesize monitors either directly from specifications in the extended temporal logic, or from NL descriptions.
Medical image segmentation plays a critical role in both image interpretation and disease diagnosis. Data-driven approaches such as U-Net have significantly advanced the field by enabling pixel-level classification of anatomical structures. However, the resulting segmentation masks often fail to comply with spatial anatomical constraints. Although properties such as organ connectedness and relative position are well understood by experts, current segmentation practices lack a systematic and explicit means to express, incorporate, or monitor this domain knowledge. In this work, we conduct a systematic study of formal specification rules across diverse medical imaging tasks with domain experts. Based on our analysis, we introduce Image Segmentation Logic (ISL), a novel spatial formalism designed to bridge the gap between expert knowledge and automated analysis. This logic provides an expressive and interpretable framework to specify critical domain knowledge and spatial constraints, and to automatically monitor their satisfaction with segmentation outputs. It integrates variables such as intensity, predicted class labels, confidence scores, and directional relationships, enabling both pixel-level and region-level specification checking. To support practical adoption, we develop an efficient monitoring tool for evaluating segmentation outputs against ISL specifications and formally prove the soundness and correctness of ISL's semantics. We demonstrate the expressiveness and utility of ISL through two case studies on established medical image segmentation datasets. Our results show that ISL enables precise detection of segmentation violations and provides more fine-grained validation than traditional metrics.
Runtime enforcement ensures that a running system complies with a property by observing and modifying the system's actions. In practice, the property is often defined in terms of high-level, abstract events, while the system's behavior consists of low-level, concrete actions. The relationship between actions and events is established in the instrumentation process, where developers must ensure that (i) system actions report the right events, and (ii) the necessary modifications to the system's behavior are correctly enforced. However, the abstraction gap between a high-level property and low-level actions makes this process error-prone. In this paper, we refine an existing formal model of runtime enforcement, which leaves instrumentation implicit, into a more precise model that explicitly accounts for instrumentation. We propose a correctness criterion for instrumentation and present a novel library, called INSTRLIB, that instruments Python applications for runtime enforcement.
Systems that adapt to their environment or change based on new requirements pose challenges for runtime verification. Complexity is increased when the system needs to retain its internal state and continue monitoring while also updating properties or adding new ones during runtime. In this work, we propose DynSRV, a Stream Runtime Verification language that allows for dynamic updates of properties. A core benefit of this language is its capability to update properties at runtime without requiring a restart of the monitor, maintaining the internal state of the remaining properties. We formalise the semantics of our core primitives and demonstrate design patterns for allowing adaptations under certain constraints. Finally, we present an implementation of DynSRV and describe three memory strategies that balance memory usage and the ability to resolve dynamically added properties depending on historical data.
As the deployment of autonomous robots expands, relying on complex decision-making policies – whether handcrafted or learned – raises concerns about their reliability. These policies are susceptible to vulnerabilities and bugs that can compromise operational integrity. This case study focuses on monitoring robotic navigation tasks, where a robot, driven by a black-box controller, must navigate towards a target. We compare three progress criteria – a simple distance metric and two variants of a stability certificate – and three finite horizon roll-out failure criteria. In laboratory experiments in both a free-space and an obstacle-field environment, one criterion combination detects true failures early with a low number of false alarms and outperforms classical heuristics at minimal computational cost. Our monitor uses only the filtered state and a finite horizon roll-out, providing formal progress/failure guarantees with low computational overhead.
The behavior of complex organisms or systems is often stored as time series data. Time series data is valuable because it contains valuable information in the form of timed patterns. However, this patterns are difficult to formalize and to detect. We present Extended Timed Regular Expressions (ETRE) to express complex timed patterns which can be systematically and efficiently matched in large sets of time series data. We translate ETRE to Timed Automata (TA), where pattern matching is computed by reachability analysis in TA. We implement our theory using C++ in the new tool TimeRex. Our tool can be used for online (run time) or offline (post processing) pattern matching. We run extensive experiments on real data. We have been able to efficiently match a number of relevant patterns.
Runtime Verification (RV) is a formal method used to check whether the execution of a system adheres to a given specification. While extensive research has focused on developing foundational theories and tools-as well as domain-specific applications, such as in the space or automotive industries-the benefits of RV in the context of general-purpose software system development remain relatively underexplored. In this paper, we propose a flexible and generic workflow for integrating RV into the development and verification processes of general-purpose software systems. We designed and implemented a prototypical RV framework based on TeSSLa, a stream-based runtime verification specification language, to monitor elicited requirements. Our approach was applied in a case study on ValiBridge, an internal software tool developed by Infineon Austria to facilitate information exchange among stakeholders involved in post-silicon verification, where it was able to detect a previously unknown bug in the software. We analyze the impact of the RV setup on development efficiency and compare its effectiveness against an existing unit test suite.
We propose a monitoring approach for hyperproperties where the system's observations range over infinite domains. The specifications are given as formulas of symbolic hypernode logic, anextension of earlier versions of hypernode logic that supports events with data. We demonstrate how to translate terms of symbolic hypernode logic into multi-tape symbolic transducers and we present a monitoring algorithm for universally quantified formulas that is based on this translation. We evaluate our approach against the previous approach for monitoring hypernode logic, and we also compare it to other monitors for hyperproperties.
Runtime Verification (RV) allows monitoring the behaviors of a system while checking them against a formal specification. The executions of distributed systems are often modeled using interleaving semantics, where events of different processes are interleaved into a total order. However, certain behavioral properties are difficult to express using interleaving semantics, whereas they can be naturally expressed in terms of partial order semantics. We study the problem of runtime verification for distributed systems based on the global states structure associated with a partial order execution. We present two algorithms for RV with branching temporal specifications and study the complexity of this problem. The first algorithm is for a global temporal logic with past operators we term PaCTL (for Past CTL). It involves constructing the branching structure of global states. We then show a second, more efficient, algorithm, for a subset of this logic that we term PaBTL. This algorithm does not require constructing the branching structure. We present implementations for both algorithms with experimental results.
The superior performance of neural networks (NNs) in safety-critical situations like automated driving (AD) vision is challenged by so-called out-of-distribution (OoD) examples: These are samples that are improbable according to the training data's distribution, such as novel object classes. In such unusual cases, NNs are prone to produce erroneous predictions with high confidence. Therefore, real-time capable localization of OoD areas in input images is needed, enabling appropriate caution if OoD locations conflict with the AD trajectory. A promising direction is computationally efficient hidden-layer "distribution-based" OoD monitoring methods. They model the activation values of neurons in a given hidden layer of the NN (so-called latent features) using probability distributions. During runtime, they then flag images yielding low probability as OoD. These methods have been successfully applied to classification, but neither to OoD localization nor object segmentation NNs. This paper investigates how far these monitoring techniques can be adapted to OoD localization and performs an extensive case study with several monitoring techniques. Additionally, we examine potential influence factors like NN architecture and training data. Our results demonstrate that this is a promising direction for efficient OoD localization.
In this paper we introduce the notion of a runtime consultant. A runtime consultant is defined with respect to some value function on infinite words. Similar to a runtime monitor, it runs in parallel to an execution of the system and provides inputs at every step of the run. While a runtime monitor alerts when a violation occurs, the idea behind a consultant is to be pro-active and provide recommendations for which action to take next in order to avoid violation (or obtain a maximal value for quantitative objectives). It is assumed that a runtime-controller can take these recommendations into consideration. The runtime consultant does not assume that its recommendations are always followed. Instead, it adjusts to the actions actually taken (similar to a vehicle navigation system). We show how to compute a runtime consultant for common value functions used in verification, and that almost all have a runtime consultant that works in constant time. We also develop consultants for $ω$-regular properties, under both their classical Boolean semantics and their recently proposed quantitative interpretation.
This paper presents an adapter for RTLOLA that simplifies the integration of runtime verification into Robot Operating System (ROS) applications. While ROS is the standard middleware for robotic development, ensuring the safety and reliability of high-level tasks such as navigation and object recognition remains challenging. The adapter facilitates the use of RTLOLA, a stream-based specification language for defining complex real-time properties, by automatically connecting a generated RTLOLA monitor to ROS topics and services. As a use case, the adapter was deployed onboard of an unmanned aircraft to reduce false positives in detecting people near the landing site. Specifically, our RTLOLA monitor cross-validates machine-learning-based person detections against objects in LiDAR depth images using classical computer vision techniques. This experiment demonstrates that runtime verification improves robotic safety while requiring minimal integration effort.
In a recent work, Bakhirkin and Basset [3] proposed a new specification language that extends STL. Their logic overcomes the syntactic restrictions of STL, enabling the production and manipulation of real-valued output signals and the expression of properties that have typically been described using other logics, such as STL*. In this contribution, we extend this specification language in three directions. First, we introduce a novel integral operator over sliding windows, allowing the specification of cumulative properties, for example, asserting that the integral of a signal over a time interval remains within a given threshold. Second, we introduce a filtering operator for the sliding window operator, enabling us to restrict the scope of aggregation to signal segments that satisfy the filtering condition. Third, we develop an efficient online monitoring algorithm for the extended logic. Finally, we test the logic on two case studies: an artificial pancreas controller and a monitoring of outdoor weather events.
Runtime verification (RV) allows monitoring executions of systems against formal specifications. A major challenge in increasing the capabilities and scope of formal methods stems from the tradeoff in increasing the expressiveness of the specification formalism used, while taming down the complexity of the involved algorithms and preserving the succinctness of the specifications. The focus of RV on a single execution at a time allows great flexibility in the way RV is implemented and towards achieving these goals. We focus here on the possibilities for implementing RV logics as external DSLs (Domain-Specific Languages), internal DSLs, and hybrid DSLs - a mix of the two. We also address the use of AI to generate monitors from natural language requirements. We survey the possibilities and focus in particular on the effect it has on achieving a desired level of expressiveness. A concrete challenge on which we focus here is allowing the use of arithmetic operations and relations on data that appear in the monitored events.
We consider the problem of quantitative predictive monitoring (QPM) of stochastic systems, i.e., predicting at runtime the degree of satisfaction of a desired temporal logic property from the current state of the system. Since computational efficiency is key to enable timely intervention against predicted violations, several state-of-the-art QPM approaches rely on fast machine-learning surrogates to provide prediction intervals for the satisfaction values, using conformal inference to offer statistical guarantees. However, these QPM methods suffer when the monitored agent exhibits multi-modal dynamics, whereby certain modes may yield high satisfaction values while others critically violate the property. Existing QPM methods are mode-agnostic and so would yield overly conservative and uninformative intervals that lack meaningful mode-specific satisfaction information. To address this problem, we present GenQPM, a method that leverages deep generative models, specifically score-based diffusion models, to reliably approximate the probabilistic and multi-modal system dynamics without requiring explicit model access. GenQPM employs a mode classifier to partition the predicted trajectories by dynamical mode. For each mode, we then apply conformal inference to produce statistically valid, mode-specific prediction intervals. We demonstrate the effectiveness of GenQPM on a benchmark of agent navigation and autonomous driving tasks, resulting in prediction intervals that are significantly more informative (less conservative) than mode-agnostic baselines.
Runtime verification encompasses several lightweight techniques for checking whether a system's current execution satisfies a given specification. We focus on runtime verification for Linear Temporal Logic (LTL). Previous work describes monitors which produce, at every time step one of three outputs - true, false, or inconclusive - depending on whether the observed execution prefix definitively determines satisfaction of the formula. However, for many LTL formulas, such as liveness properties, satisfaction cannot be concluded from any finite prefix. For these properties traditional monitors will always output inconclusive. In this work, we propose a novel monitoring approach that replaces hard verdicts with probabilistic predictions and an associated confidence score. Our method guarantees eventual correctness of the prediction and ensures that confidence increases without bound from that point on.
Formal verification provides assurances that a probabilistic system satisfies its specification-conditioned on the system model being aligned with reality. We propose alignment monitoring to watch that this assumption is justified. We consider a probabilistic model well aligned if it accurately predicts the behaviour of an uncertain system in advance. An alignment score measures this by quantifying the similarity between the model's predicted and the system's (unknown) actual distributions. An alignment monitor observes the system at runtime; at each point in time it uses the current state and the model to predict the next state. After the next state is observed, the monitor updates the verdict, which is a high-probability interval estimate for the true alignment score. We utilize tools from sequential forecasting to construct our alignment monitors. Besides a monitor for measuring the expected alignment score, we introduce a differential alignment monitor, designed for comparing two models, and a weighted alignment monitor, which permits task-specific alignment monitoring. We evaluate our monitors experimentally on the PRISM benchmark suite. They are fast, memory-efficient, and detect misalignment early.
Fairness in AI is traditionally studied as a static property evaluated once, over a fixed dataset. However, real-world AI systems operate sequentially, with outcomes and environments evolving over time. This paper proposes a framework for analysing fairness as a runtime property. Using a minimal yet expressive model based on sequences of coin tosses with possibly evolving biases, we study the problems of monitoring and enforcing fairness expressed in either toss outcomes or coin biases. Since there is no one-size-fits-all solution for either problem, we provide a summary of monitoring and enforcement strategies, parametrised by environment dynamics, prediction horizon, and confidence thresholds. For both problems, we present general results under simple or minimal assumptions. We survey existing solutions for the monitoring problem for Markovian and additive dynamics, and existing solutions for the enforcement problem in static settings with known dynamics.
Stream-based monitoring is a well-established runtime verification approach which relates input streams, representing sensor readings from the monitored system, with output streams that capture filtered or aggregated results. In such approaches, the monitor is a passive external component that continuously receives sensor data from the system under observation. This setup assumes that the system dictates what data is sent and when, regardless of the monitor's current needs. However, in many applications – particularly in resource-constrained environments like autonomous aircraft, where energy, size, or weight are limited – this can lead to inefficient use of communication resources. We propose making the monitor an active component that decides, based on its current internal state, which sensors to query and how often. This behavior is driven by scheduling annotations in the specification, which guide the dynamic allocation of bandwidth towards the most relevant data, thereby improving monitoring efficiency. We demonstrate our approach using the stream-based specification language RTLola and assess the performance by monitoring a specification from the aerospace domain. With equal bandwidth usage, our approach detects specification violations significantly sooner than monitors sampling all inputs at a fixed frequency.
We propose a novel framework that harnesses the power of generative artificial intelligence and copula-based modeling to address two critical challenges in multivariate time-series analysis: delivering accurate predictions and enabling robust anomaly detection. Our method, Copula-based Conformal Anomaly Identification for Multivariate Time-Series (CoCAI), leverages a diffusion-based model to capture complex dependencies within the data, enabling high quality forecasting. The model's outputs are further calibrated using a conformal prediction technique, yielding predictive regions which are statistically valid, i.e., cover the true target values with a desired confidence level. Starting from these calibrated forecasts, robust outlier detection is performed by combining dimensionality reduction techniques with copula-based modeling, providing a statistically grounded anomaly score. CoCAI benefits from an offline calibration phase that allows for minimal overhead during deployment and delivers actionable results rooted in established theoretical foundations. Empirical tests conducted on real operational data derived from water distribution and sewerage systems confirm CoCAI's effectiveness in accurately forecasting target sequences of data and in identifying anomalous segments within them.
