Please use this identifier to cite or link to this item:
https://www.um.edu.mt/library/oar/handle/123456789/85901
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. |
URI: | https://www.um.edu.mt/library/oar/handle/123456789/85901 |
Appears in Collections: | Scholarly Works - FacICTCS |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
The Best a Monitor Can Do.pdf | 723.77 kB | Adobe PDF | View/Open |
Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.