Adventures in monitorability: From branching time to linear time and back again.



Aceto, Luca, Achilleos, Antonis, Francalanza, Adrian, Ingolfdottir, Anna and Lehtinen, MK ORCID: 0000-0003-1171-8790
(2019) Adventures in monitorability: From branching time to linear time and back again. Proceedings of the ACM on Programming Languages, 3 (POPL). pp. 1-29.

[img] Text
1902.00435v1.pdf - Published version

Download (802kB) | Preview

Abstract

This paper establishes a comprehensive theory of runtime monitorability for Hennessy-Milner logic with recursion, a very expressive variant of the modal µ-calculus. It investigates the monitorability of that logic with a linear-time semantics and then compares the obtained results with ones that were previously presented in the literature for a branching-time setting. Our work establishes an expressiveness hierarchy of monitorable fragments of Hennessy-Milner logic with recursion in a linear-time setting and exactly identifies what kinds of guarantees can be given using runtime monitors for each fragment in the hierarchy. Each fragment is shown to be complete, in the sense that it can express all properties that can be monitored under the corresponding guarantees. The study is carried out using a principled approach to monitoring that connects the semantics of the logic and the operational semantics of monitors. The proposed framework supports the automatic, compositional synthesis of correct monitors from monitorable properties.

Item Type: Article
Additional Information: Published in POPL 2019. 54 pages, including the appendix
Uncontrolled Keywords: monitorability, linear-time and branching-time logics, monitor synthesis
Depositing User: Symplectic Admin
Date Deposited: 08 Jun 2020 09:03
Last Modified: 17 Mar 2024 05:34
DOI: 10.1145/3290365
Related URLs:
URI: https://livrepository.liverpool.ac.uk/id/eprint/3089575