Standard
Multi-head Monitoring of Metric Dynamic Logic. / Raszyk, Martin; Basin, David; Traytel, Dmitriy.
Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings. red. / Dang Van Hung; Oleg Sokolsky. Springer, 2020. s. 233-250 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 12302 LNCS).
Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Harvard
Raszyk, M, Basin, D
& Traytel, D 2020,
Multi-head Monitoring of Metric Dynamic Logic. i DV Hung & O Sokolsky (red),
Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings. Springer, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), bind 12302 LNCS, s. 233-250, 18th International Symposium on Automated Technology for Verification and Analysis, ATVA 2020, Hanoi, Vietnam,
19/10/2020.
https://doi.org/10.1007/978-3-030-59152-6_13APA
Raszyk, M., Basin, D.
, & Traytel, D. (2020).
Multi-head Monitoring of Metric Dynamic Logic. I D. V. Hung, & O. Sokolsky (red.),
Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings (s. 233-250). Springer. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Bind 12302 LNCS
https://doi.org/10.1007/978-3-030-59152-6_13Vancouver
Raszyk M, Basin D
, Traytel D.
Multi-head Monitoring of Metric Dynamic Logic. I Hung DV, Sokolsky O, red., Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings. Springer. 2020. s. 233-250. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 12302 LNCS).
https://doi.org/10.1007/978-3-030-59152-6_13Author
Raszyk, Martin ; Basin, David ; Traytel, Dmitriy. / Multi-head Monitoring of Metric Dynamic Logic. Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings. red. / Dang Van Hung ; Oleg Sokolsky. Springer, 2020. s. 233-250 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 12302 LNCS).
Bibtex
@inproceedings{361418bc6158413c848d217ed43a4f8b,
title = "Multi-head Monitoring of Metric Dynamic Logic",
abstract = "We develop a monitoring algorithm for metric dynamic logic, an extension of metric temporal logic with regular expressions. The monitor computes whether a given formula is satisfied at every position in an input trace of time-stamped events. Our monitor follows the multi-head paradigm: it reads the input simultaneously at multiple positions and moves its reading heads asynchronously. This mode of operation results in unprecedented space complexity guarantees for metric dynamic logic: The monitor{\textquoteright}s memory consumption neither depends on the event-rate, i.e., the number of events within a fixed time-unit, nor on the numeric constants occurring in the quantitative temporal constraints in the given formula. We formally prove our algorithm correct in the Isabelle proof assistant, integrate it in the Hydra monitoring tool, and empirically demonstrate its strong performance.",
author = "Martin Raszyk and David Basin and Dmitriy Traytel",
year = "2020",
doi = "10.1007/978-3-030-59152-6_13",
language = "English",
isbn = "9783030591519",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "233--250",
editor = "Hung, {Dang Van} and Oleg Sokolsky",
booktitle = "Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings",
address = "Switzerland",
note = "18th International Symposium on Automated Technology for Verification and Analysis, ATVA 2020 ; Conference date: 19-10-2020 Through 23-10-2020",
}
RIS
TY - GEN
T1 - Multi-head Monitoring of Metric Dynamic Logic
AU - Raszyk, Martin
AU - Basin, David
AU - Traytel, Dmitriy
PY - 2020
Y1 - 2020
N2 - We develop a monitoring algorithm for metric dynamic logic, an extension of metric temporal logic with regular expressions. The monitor computes whether a given formula is satisfied at every position in an input trace of time-stamped events. Our monitor follows the multi-head paradigm: it reads the input simultaneously at multiple positions and moves its reading heads asynchronously. This mode of operation results in unprecedented space complexity guarantees for metric dynamic logic: The monitor’s memory consumption neither depends on the event-rate, i.e., the number of events within a fixed time-unit, nor on the numeric constants occurring in the quantitative temporal constraints in the given formula. We formally prove our algorithm correct in the Isabelle proof assistant, integrate it in the Hydra monitoring tool, and empirically demonstrate its strong performance.
AB - We develop a monitoring algorithm for metric dynamic logic, an extension of metric temporal logic with regular expressions. The monitor computes whether a given formula is satisfied at every position in an input trace of time-stamped events. Our monitor follows the multi-head paradigm: it reads the input simultaneously at multiple positions and moves its reading heads asynchronously. This mode of operation results in unprecedented space complexity guarantees for metric dynamic logic: The monitor’s memory consumption neither depends on the event-rate, i.e., the number of events within a fixed time-unit, nor on the numeric constants occurring in the quantitative temporal constraints in the given formula. We formally prove our algorithm correct in the Isabelle proof assistant, integrate it in the Hydra monitoring tool, and empirically demonstrate its strong performance.
U2 - 10.1007/978-3-030-59152-6_13
DO - 10.1007/978-3-030-59152-6_13
M3 - Article in proceedings
AN - SCOPUS:85093863993
SN - 9783030591519
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 233
EP - 250
BT - Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings
A2 - Hung, Dang Van
A2 - Sokolsky, Oleg
PB - Springer
T2 - 18th International Symposium on Automated Technology for Verification and Analysis, ATVA 2020
Y2 - 19 October 2020 through 23 October 2020
ER -
