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

Displayed 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
22m
Talk
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
22m
Talk
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
22m
Talk
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