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 Jan Times are displayed in time zone: Greenwich Mean Time : Belfast change
13:45 - 14:51: Model CheckingResearch Papers at Sala II Chair(s): P. MadhusudanUniversity of Illinois at Urbana-Champaign | |||
13:45 - 14:07 Talk | Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations Research Papers Taolue ChenBirkbeck, University of London, Matthew HagueRoyal Holloway, University of London, Anthony Widjaja LinOxford University, Philipp RuemmerUppsala University, Zhilin WuState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences Link to publication DOI Media Attached File Attached | ||
14:07 - 14:29 Talk | Bounded Model Checking of Signal Temporal Logic Properties Using Syntactic Separation Research Papers Kyungmin BaePohang University of Science and Technology (POSTECH), Jia LeePohang University of Science and Technology (POSTECH) Link to publication DOI Media Attached File Attached | ||
14:29 - 14:51 Talk | Adventures in Monitorability: From Branching to Linear Time and Back Again Research Papers Luca AcetoReykjavik University, Antonis AchilleosReykjavik University, Adrian FrancalanzaUniversity of Malta, Anna IngolfsdottirReykjavik University, Karoliina LehtinenUniversity of Kiel and University of Liverpool Link to publication DOI Media Attached |