2026-10-09T01:03:52Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23954 2026-08-31T10:17:31Z ddc:004 open_access

Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory Aceto, Luca Achilleos, Antonis Attard, Duncan Paul Exibard, Léo Francalanza, Adrian Ingólfsdóttir, Anna Lehtinen, Karoliina Runtime verification monitorability μHML with data register automata Runtime verification consists in checking whether a system satisfies a given specification by observing the execution trace it produces. In the regular setting, the modal μ-calculus provides a versatile formalism for expressing specifications of the control flow of the system. This paper focuses on the data flow and studies an extension of that logic that allows it to express data-dependent properties, identifying fragments that can be verified at runtime and with what correctness guarantees. The logic studied here is closely related with register automata with guessing. That correspondence yields a monitor synthesis algorithm, and a strict hierarchy among the various fragments of the logic, in contrast to the regular setting. We then exhibit a fragment of the logic that can express all monitorable formulae in the logic without greatest fixed-points but not in the full logic, and show this is the best we can get. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Luca Aceto and Antonis Achilleos and Duncan Paul Attard and Léo Exibard and Adrian Francalanza and Anna Ingólfsdóttir and Karoliina Lehtinen 2025 Is Part Of LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2025.4 urn:nbn:de:0030-drops-239546 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.4 eng https://creativecommons.org/licenses/by/4.0/legalcode