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
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
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
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
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