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 JunDisplayed 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 21mTalk | 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 21mTalk | 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 21mTalk | 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 21mTalk | The Algebra of Patterns Technical Papers | ||
12:24 21mTalk | 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 |