Back to overview

Almost Event-Rate Indepedent Monitoring of Metric Temporal Logic

Type of publication Peer-reviewed
Publikationsform Proceedings (peer-reviewed)
Author Basin David, Bhatt Bhargav Nagaraja, Traytel Dmitriy,
Project Big Data Monitoring
Show all

Proceedings (peer-reviewed)

Editor , Margaria Tiziana; , Legay Axel
Volume (Issue) 10206
Page(s) 94 - 112
Title of proceedings {TACAS} 2017
DOI 10.1007/978-3-662-54580-5_6


A monitoring algorithm is trace-length independent if its space consumption does not depend on the number of events processed. The analysis of many monitoring algorithms has aimed at establishing trace-length independence. But a trace-length independent monitor’s space consumption can depend on characteristics of the trace other than its size. We put forward the stronger notion of event-rate independence, where the monitor’s space usage does not depend on the event rate. This property is critical for monitoring voluminous streams of events arriving at a varying rate. Some previously proposed algorithms for past-only temporal logics satisfy this new property. However, when dealing with future operators, the traditional approach of using a queue to wait for future obligations to be resolved is not event-rate independent. We propose a new algorithm that supports metric past and bounded future operators and is almost event-rate independent, where "almost" denotes a logarithmic dependence on the event rate: the algorithm must store the event rate as a number. We compare our algorithm with traditional ones, providing evidence that almost event-rate independence matters in practice.