Efficient Offline Monitoring of Linear Temporal Logic with Bit Vectors

TL;DR

This paper introduces a bitmap-based offline verification method for Linear Temporal Logic (LTL) that enables high-speed evaluation of complex formulas on event traces, achieving millions of events per second.

Contribution

It presents a novel bitmap manipulation technique for efficient offline LTL verification, significantly improving processing speed for complex formulas.

Findings

Supports complex LTL formulas with nearly 20 operators

Achieves evaluation throughput of millions of events per second

Demonstrates efficiency of bitmap-based offline verification

Abstract

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.