A bitmap is a data structure designed to compactly represent sets of integers; it provides very fast operations for querying and manipulating such sets, exploiting bit-level parallelism. In this paper, we describe a technique for the offline verification of arbitrary expressions of Linear Temporal Logic using bitmap manipulation. An event trace is first preprocessed and transformed into a set of bitmaps. The LTL expression is then evaluated through a recursive procedure manipulating these bitmaps. Experimental results show that, for complex LTL formulas containing almost 20 operators, event traces can be evaluated at a throughput of millions of events per second.
@article{arxiv.2005.11737,
title = {Efficient Offline Monitoring of Linear Temporal Logic with Bit Vectors},
author = {Kun Xie and Sylvain Hallé},
journal= {arXiv preprint arXiv:2005.11737},
year = {2020}
}