The cost of monitoring alone

Luca Aceto, Antonis Achilleos*, Adrian Francalanza, Anna Ingólfsdóttir, Karoliina Lehtinen

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review

2 Citations (Scopus)

Abstract

We compare the succinctness of two monitoring systems for properties of infinite traces, namely parallel and regular monitors. Although a parallel monitor can be turned into an equivalent regular monitor, the cost of this transformation is a double-exponential blowup in the syntactic size of the monitors, and a triple-exponential blowup when the goal is a deterministic monitor. We show that these bounds are tight and that they also hold for translations between corresponding fragments of Hennessy-Milner logic with recursion over infinite traces.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer-Verlag
Pages259-275
Number of pages17
DOIs
Publication statusPublished - 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11500 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Bibliographical note

Funding Information:
This research was partially supported by the projects “TheoFoMon: Theoretical Foundations for Monitorability” (grant number: 163406-051) and “Epistemic Logic for Distributed Runtime Monitoring” (grant number: 184940-051) of the Icelandic Research Fund, by the BMBF project “Aramis II” (project number: 01IS160253) and the EPSRC project “Solving parity games in theory and practice” (project number: EP/P020909/1).

Publisher Copyright:
© Springer Nature Switzerland AG 2019.

Other keywords

  • Determinization
  • Hennessy Milner logic with recursion
  • Logical fragments
  • Monitors
  • Runtime Verification
  • State complexity

Fingerprint

Dive into the research topics of 'The cost of monitoring alone'. Together they form a unique fingerprint.

Cite this