DejaVu: A Monitoring Tool for First-Order Temporal Logic

In this paper, we describe our monitoring tool, DejaVu, which implements our algorithm for monitoring first-order past linear-time temporal logic over a sequence of events that carry data. We propose the use of Binary Decision Diagrams (BDDs) for representing and manipulating sets of observed data since (1) BDDs provide highly compact representations, (2) operations overBDDs, in particular complementation, are very efficient, and (3) the monitor construction for the propositional case shown in naturally extends to BDDs. Our experiments show a substantial improvement in performance compared to a related tool.