Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Fri 18 Jan 2019 14:29 - 14:51 at Sala II - Model Checking Chair(s): P. Madhusudan

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

POPL-2019-Research-Papers
13:45 - 14:51: Research Papers - Model Checking at Sala II
Chair(s): P. MadhusudanUniversity of Illinois at Urbana-Champaign
POPL-2019-Research-Papers13:45 - 14:07
Talk
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
POPL-2019-Research-Papers14:07 - 14:29
Talk
Kyungmin BaePohang University of Science and Technology (POSTECH), Jia LeePohang University of Science and Technology (POSTECH)
Link to publication DOI Media Attached File Attached
POPL-2019-Research-Papers14:29 - 14:51
Talk
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