Multi-head Monitoring of Metric Dynamic Logic
Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Dokumenter
- Fulltext
Accepteret manuskript, 404 KB, PDF-dokument
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.
Originalsprog | Engelsk |
---|---|
Titel | Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings |
Redaktører | Dang Van Hung, Oleg Sokolsky |
Forlag | Springer |
Publikationsdato | 2020 |
Sider | 233-250 |
ISBN (Trykt) | 9783030591519 |
DOI | |
Status | Udgivet - 2020 |
Begivenhed | 18th International Symposium on Automated Technology for Verification and Analysis, ATVA 2020 - Hanoi, Vietnam Varighed: 19 okt. 2020 → 23 okt. 2020 |
Konference
Konference | 18th International Symposium on Automated Technology for Verification and Analysis, ATVA 2020 |
---|---|
Land | Vietnam |
By | Hanoi |
Periode | 19/10/2020 → 23/10/2020 |
Navn | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Vol/bind | 12302 LNCS |
ISSN | 0302-9743 |
ID: 258453436