Please use this identifier to cite or link to this item:
Title: The best a monitor can do
Authors: Aceto, Luca
Achilleos, Antonis
Francalanza, Adrian
Ingólfsdóttir, Anna
Lehtinen, Karoliina
Keywords: Software engineering
Computer software -- Verification
Object monitors (Computer software)
Computer logic
Issue Date: 2021
Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik GmbH
Citation: Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., & Lehtinen, K. (2021). The best a monitor can do. 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), Ljubljana. 1-23.
Abstract: 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.
Appears in Collections:Scholarly Works - FacICTCS

Files in This Item:
File Description SizeFormat 
The Best a Monitor Can Do.pdf723.77 kBAdobe PDFView/Open

Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.