Tehran Institute for Advanced Studies (TEIAS)

/ An Operational Guide to Monitorability __ Luca Aceto


An Operational Guide to Monitorability


February 24, 2021
(06 Esfand, 1399)



This Talk is online

Registration Deadline

February 23, 2021


Luca Aceto

Reykjavik University and Gran Sasso Science Institute, L’Aquila



Monitorability underpins the technique of Runtime Verification because it delineates what properties can be verified at runtime. Although many definitions of monitorability exist, few are defined explicitly in terms of the operational guarantees provided by monitors, which are the computational entities carrying out the verification. We view monitorability as a spectrum, where the fewer guarantees that are required of monitors, the more properties become monitorable. Accordingly, we present a monitorability hierarchy based on this trade-off. For regular specifications, we give syntactic characterisations in Hennessy–Milner logic with recursion for its levels. Finally, we map existing monitorability definitions into our hierarchy. Our work gives a unified framework that makes the operational asumtions and guarantees of each definition explicit. This provides a rigorous foundation that can inform design choices and correctness claims for runtime verification tools. This presentation is based on joint work with Antonis Achilles (Reykjavik University), Adrian Francalanza (University of Malta), Anna Ingólfsdótt (Reykjavik University) and Karoliina Lehtinen (University of Liverpool).



Luca Aceto is a professor of Computer Science at Reykjavik University, Iceland, and at the Gran Sasso Science Institute, L’Aquila, Italy. Previously, he held permanent academic positions at the University of Sussex, UK, and at Aalborg University, Denmark. He is an elected member of Academia European, the Academy of Europe. He was the President of the European Association for Theoretical Computer Science from July 2012 till July 2016, and a co-founder and first chair of the IFIP WG 1.8 on Concurrency Theory. He currently serves as the chair of the editorial board of LIPIcs. Luca Aceto’s research has mostly focused on concurrency theory (with emphasis on process calculi), structural operational semantics, logic in computer science and runtime monitoring. He received a Distinguished Dissertation Award of the British Computer Society in 1991 and the Reykjavik University Research Award in 2012.