The Best a Monitor Can Do

Medientyp: E-Artikel; Elektronischer Konferenzbericht; Sonstige Veröffentlichung

Titel: The Best a Monitor Can Do

Beteiligte: Aceto, Luca [VerfasserIn]; Achilleos, Antonis [VerfasserIn]; Francalanza, Adrian [VerfasserIn]; Ingólfsdóttir, Anna [VerfasserIn]; Lehtinen, Karoliina [VerfasserIn]

Erschienen: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021

Sprache: Englisch

DOI: https://doi.org/10.4230/LIPIcs.CSL.2021.7

Schlagwörter: branching-time logics ; monitorability ; runtime verification

Entstehung:

Anmerkungen: Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.

Beschreibung: Existing notions of monitorability for branching-time properties are fairly restrictive. This, in turn, impacts the ability to incorporate prior knowledge about the system under scrutiny - which corresponds to a branching-time property - into the runtime analysis. We propose a definition of optimal monitors that verify the best monitorable under- or over-approximation of a specification, regardless of its monitorability status. Optimal monitors can be obtained for arbitrary branching-time properties by synthesising a sound and complete monitor for their strongest monitorable consequence. We show that the strongest monitorable consequence of specifications expressed in Hennessy-Milner logic with recursion is itself expressible in this logic, and present a procedure to find it. Our procedure enables prior knowledge to be optimally incorporated into runtime monitors.

Zugangsstatus: Freier Zugang

Nur in Feld suchen:

Zuletzt gesuchte Begriffe: