Abstract | ||
---|---|---|
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. |
Year | DOI | Venue |
---|---|---|
2018 | 10.1109/MT-CPS.2018.00013 | 2018 IEEE Workshop on Monitoring and Testing of Cyber-Physical Systems (MT-CPS) |
Keywords | Field | DocType |
BDD,temporal-logic,monitoring,runtime-verification | First order,Computer science,Binary decision diagram,Theoretical computer science,Temporal logic,Encoding (memory) | Conference |
ISBN | Citations | PageRank |
978-1-5386-6749-1 | 0 | 0.34 |
References | Authors | |
3 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Klaus Havelund | 1 | 3522 | 254.55 |
Doron Peled | 2 | 3357 | 273.18 |
Dogan Ulus | 3 | 45 | 6.11 |