Adventures in Monitorability: From Branching to Linear Time and Back Again
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.
Fri 18 JanDisplayed time zone: Belfast change
13:45 - 14:51 | Model CheckingResearch Papers at Sala II Chair(s): P. Madhusudan University of Illinois at Urbana-Champaign | ||
13:45 22mTalk | Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations Research Papers Taolue Chen Birkbeck, University of London, Matthew Hague Royal Holloway, University of London, Anthony Widjaja Lin Oxford University, Philipp Ruemmer Uppsala University, Zhilin Wu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences Link to publication DOI Media Attached File Attached | ||
14:07 22mTalk | Bounded Model Checking of Signal Temporal Logic Properties Using Syntactic Separation Research Papers Kyungmin Bae Pohang University of Science and Technology (POSTECH), Jia Lee Pohang University of Science and Technology (POSTECH) Link to publication DOI Media Attached File Attached | ||
14:29 22mTalk | Adventures in Monitorability: From Branching to Linear Time and Back Again Research Papers Luca Aceto Reykjavik University, Antonis Achilleos Reykjavik University, Adrian Francalanza University of Malta, Anna Ingolfsdottir Reykjavik University, Karoliina Lehtinen University of Kiel and University of Liverpool Link to publication DOI Media Attached |