understanding and pushing the limits of monitoring in a real-time setting
Runtime monitoring has gained acceptance as a method for formally verifying
the correctness of executing systems. Monitoring means to test a sequence of
observations of a system against a specification, often written in a formal logic.
Monitoring contrasts with static verification methods, like model checking, in
that it is computationally easier due to only testing a single system execution.
Runtime monitoring may also be applied to black-box systems where details
about the environment and design of the monitored system are not required to
be known in advance.
Monitoring realistic systems requires handling data loss and corruption.
Typically, theory ignores these realistic constraints and assumes perfect conditions, but we developed new theory to model the effects of trace mutations and decide if a property can be monitored under known imperfect conditions (Kauffman et al., 2019).
By separating the results by the type of monitor verdict, we showed that many properties are still monitorable for some verdicts even under arbitrary loss or message reordering (Kauffman et al., 2021).
Many systems have so-called “extra-functional” requirements that must be
expressed with respect to time. These systems, generally called real-time systems,
are pervasive in modern life as the controllers of cyber-physical systems. To
express requirements with time components, logics such as Metric Temporal
Logic (MTL) and derivatives like Metric Interval Temporal Logic (MITL) have
been developed that extend the more classical Linear Temporal Logic (LTL) with
timing constraints. Finite Automata have also been extended with time
to form Timed Automata. These formalisms allow the expression of notions
such as that a response should occur within 20 milliseconds of a request.
Monitoring timed properties is possible and several solutions have been proposed,
each with their own advantages and drawbacks.
CritLab has worked with researchers at Aalborg University to develop methods and tools to monitor real-time properties (Grosen et al., 2022).
We take an automata-theoretic approach to monitor construction that supports a wide range of timed formalisms while remaining performant.
Recently, we identified for the first time the monitorability of properties expressed as timed automata with different acceptance conditions (Grosen et al., 2025).
Monitoring is an important part of the verification toolbox, in particular in situations where exhaustive verification using, e.g., model-checking is infeasible.The goal of online monitoring is to determine the satisfaction or violation of a specification during runtime, i.e., based on finite execution prefixes. However, not every specification is amenable to monitoring, e.g., properties for which no finite execution can witness satisfaction or violation. Monitorability is the question of whether a given specification is amenable to monitoring, and has been extensively studied in discrete time.
Here, we study the monitorability problem for real-time properties expressed as Timed Automata. For specifications given by deterministic Timed Muller Automata, we prove decidability while we show that the problem is undecidable for specifications given by nondeterministic Timed Büchi automata.
Furthermore, we refine monitorability to also determine bounds on the number of events as well as the time that must pass before monitoring the property may yield an informative verdict. We prove that for deterministic Timed Muller automata, such bounds can be effectively computed. In contrast we show that for nondeterministic Timed Büchi automata such bounds are not computable.
@inproceedings{grosen2025time,title={Time for Timed Monitorability},author={Grosen, Thomas M{\o}ller and Kauffman, Sean and Guldstrand Larsen, Kim and Zimmermann, Martin},booktitle={International Conference on Concurrency Theory {(CONCUR'25)}},origin={Professor},year={2025},month=aug,publisher={Schloss Dagstuhl - Leibniz-Zentrum für Informatik},isbn={978-3-95977-339-3},location={Aarhus, Denmark},note={Accepted},selected=true,preview=clock.webp}
In this paper we revisit monitoring real-time systems with respect to
properties expressed either in Metric Interval Temporal Logic or as Timed
Büchi Automata. We offer efficient symbolic online monitoring
algorithms in a number of settings, exploiting so-called zones well-known
from efficient model checking of Timed Automata. The settings considered
include new, much simplified treatment of time divergence, monitoring under
timing uncertainty, and, extension of monitoring to offer minimum time
estimates before conclusive verdicts can be made.
This article addresses the question of what properties can be monitored
over an unreliable communication channel. We model unreliable
communications as mutations to finite traces and define what it means
for a property to be immune to such a mutation. We also introduce the
idea of a trustworthy verdict, which is a verdict guaranteed to be correct
in the presence of a trace mutation. We show that the trustworthiness of
a verdict or immunity of a property for a single mutation is equivalent
to the trustworthiness or immunity for any number of mutations. We
classify trustworthy verdicts on ω-regular properties by updating
a recently proposed monitorability-focused refinement of the safety-liveness
taxonomy. The article also includes a fixed-parameter tractable algorithm
to test an ω-regular property for immunity to a trace mutation. Our
results show that many of the most common properties can be monitored over
unreliable channels.
In Runtime Verification (RV), monitoring a program means checking an
execution trace of the program for satisfactions and violations of
properties. The question of which properties can be effectively
monitored over ideal channels has mostly been answered by prior
work. However, program monitoring is often deployed for remote
systems where communications may be unreliable.
In this work, we address the question of what properties are
monitorable over an unreliable communication channel. We describe
the different types of mutations that may be introduced to an
execution trace and examine their effects on program monitoring.
We propose a fixed-parameter tractable algorithm for determining the
immunity of a finite automaton to a trace mutation and show how it
can be used to classify ω-regular properties as monitorable
over channels with that mutation.
