Back to overview

Almost Event-Rate Indepedent Monitoring of Metric Dynamic Logic

Type of publication Peer-reviewed
Publikationsform Proceedings (peer-reviewed)
Author Basin David, Krstić Srđan, Traytel Dmitriy,
Project Big Data Monitoring
Show all

Proceedings (peer-reviewed)

Editor , Reger Giles; , Lahiri Shuvendu
Page(s) 85 - 102
Title of proceedings {RV} 2017
DOI 10.1007/978-3-319-67531-2_6


Linear temporal logic (LTL) and its quantitative extension metric temporal logic (MTL) are standard languages for specifying system behaviors. Regular expressions are an even more expressive formalism in the non-metric setting and several extensions of LTL, including the recently proposed linear dynamic logic (LDL), offer regular-expression-like constructs. We extend LDL with past operators and quantitative features. The resulting metric dynamic logic (MDL) offers the quantitative temporal conveniences of MTL while increasing its expressiveness. We develop and evaluate an online monitoring algorithm for MDL whose space-consumption is almost event-rate independent—a notion that characterizes monitors that scale to high-velocity event streams.