Monitoring Timed Properties (Revisited)

TL;DR

This paper presents efficient symbolic online monitoring algorithms for real-time systems using Metric Interval Temporal Logic and Timed B"uchi Automata, addressing time divergence and timing uncertainty, implemented in the MoniTAal tool.

Contribution

It introduces a simplified approach to time divergence and uncertainty in monitoring, with algorithms and a practical implementation for long trace analysis.

Findings

Effective monitoring of long traces demonstrated

Handling of time divergence and uncertainty improved

Algorithms integrated into the MoniTAal tool

Abstract

In this paper we study monitoring of real-time systems with respect to properties expressed either in Metric Interval Temporal Logic or as Timed B\"uchi 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. Our contributions include a new, much simplified treatment of time divergence and monitoring under timing uncertainty. The online monitoring procedure that handles time divergence, as well as uncertain timing, is implemented in the tool MoniTAal, and shown to effectively monitor properties over long traces.