Trace checking of Metric Temporal Logic with Aggregating Modalities using MapReduce

TL;DR

This paper introduces a MapReduce-based algorithm for trace checking of Metric Temporal Logic with aggregating modalities, enabling scalable analysis of large execution logs for complex system specifications.

Contribution

It presents a novel parallel algorithm leveraging MapReduce to efficiently evaluate metric temporal logic with aggregate operators over large traces.

Findings

Significant reduction in evaluation time through parallelization.

Scalability demonstrated on Hadoop framework.

Effective handling of quantitative and timing constraints.

Abstract

Modern complex software systems produce a large amount of execution data, often stored in logs. These logs can be analyzed using trace checking techniques to check whether the system complies with its requirements specifications. Often these specifications express quantitative properties of the system, which include timing constraints as well as higher-level constraints on the occurrences of significant events, expressed using aggregate operators. In this paper we present an algorithm that exploits the MapReduce programming model to check specifications expressed in a metric temporal logic with aggregating modalities, over large execution traces. The algorithm exploits the structure of the formula to parallelize the evaluation, with a significant gain in time. We report on the assessment of the implementation - based on the Hadoop framework - of the proposed algorithm and comment on its scalability.