ECOOP 2025
Mon 30 June - Fri 4 July 2025 Bergen, Norway

Runtime Verification (RV) techniques are becoming increasingly popular, due to their scalability and ability to analyse block-box systems. Monitoring is at the heart of RV; a logical formula φ, formalising some property of interest, is typically translated into a monitor that checks whether the system under scrutiny satisfies φ during its execution. A logical formula φ is violation (resp. satisfaction) monitorable iff there exists a monitor for φ that is both sound and complete w.r.t. its violation (resp. satisfaction) by a system; and φ is monitorable if it is violation or satisfaction monitorable. The monitorability problem naturally arises: given a logic L, what is the largest subset of L that is monitorable? While this problem has been solved for expressive untimed logics, it remains open for timed logics, i.e., where formulae can express both the order of events and the quantity of time separating them. In this paper, we solve the monitorability problem for Tlin, a new expressive (linear-time) timed μ-calculus that we propose. First, we show that Tlin is strictly more expressive than MTL, a popular timed extension of the well-known LTL. Second, we identify MTlin, the largest monitorable fragment of Tlin; and further characterise its largest subsets of formulae that are violation monitorable, satisfaction monitorable, and complete monitorable (both satisfaction and violation monitorable). To the best of our knowledge, this is the first work that answers the monitorability question for an expressive timed logic. Our theoretical results are accompanied with compilers (i) from MTL to Tlin and (ii) from MTlin formulae to monitors.

Mon 30 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

11:00 - 12:45
Formal Methods, Logics, and Static Analysis FrameworksTechnical Papers at Auditorium M003
Chair(s): Marco Carbone IT University of Copenhagen
11:00
21m
Talk
Compositional Static Value Analysis for Higher-Order Numerical Programs
Technical Papers
Milla Valnet Sorbonne Université, Raphaël Monat Inria and University of Lille, Antoine Miné Sorbonne Université
11:21
21m
Talk
Lightweight Diagramming for Formal Methods: A Grounded Language Design
Technical Papers
Siddhartha Prasad Brown University, Ben Greenman University of Utah, Tim Nelson Brown University, Shriram Krishnamurthi Brown University
11:42
21m
Talk
Taming and Dissecting Recursions through Interprocedural Weak Topological Ordering
Technical Papers
Jiawei Yang , Xiao Cheng Macquarie University, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon, Xiapu Luo Hong Kong Polytechnic University, Yulei Sui University of New South Wales
12:03
21m
Talk
The Algebra of Patterns
Technical Papers
David Binder University of Kent, UK, Lean Ermantraut Radboud University Nijmegen
12:24
21m
Talk
A theory of (linear-time) timed monitors
Technical Papers
Mouloud Amara IRIF, Université Paris Cité, Giovanni Bernardi IRIF, Université Paris Cité, Mohammed Aristide Foughali Université Paris Cité / IRIF, Adrian Francalanza University of Malta
:
:
:
: