2026-07-23T13:42:25Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13441 2024-03-06T10:52:05Z ddc:004 open_access

The Best a Monitor Can Do Aceto, Luca Achilleos, Antonis Francalanza, Adrian Ingólfsdóttir, Anna Lehtinen, Karoliina monitorability branching-time logics runtime verification 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Luca Aceto and Antonis Achilleos and Adrian Francalanza and Anna Ingólfsdóttir and Karoliina Lehtinen 2021 Is Part Of LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2021.7 urn:nbn:de:0030-drops-134416 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.7 eng https://creativecommons.org/licenses/by/3.0/legalcode