Trace checking of metric temporal logic with aggregating modalities using MapReduce