BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//University of Liverpool Computer Science Seminar System//v2//EN
BEGIN:VEVENT
DTSTAMP:20260526T031637Z
UID:Seminar-verification-695@lxserverM.csc.liv.ac.uk
ORGANIZER:CN=Patrick Totzke:MAILTO:totzke@liverpool.ac.uk
DTSTART:20200331T110000
DTEND:20200331T120000
SUMMARY:Verification Series
DESCRIPTION:Martin Zimmermann: From LTL to rLTL Monitoring: Improved Monitorability through Robust Semantics\n\nRuntime monitoring is commonly used to detect the violation of desired properties in safety critical cyber-physical systems by observing its executions. Bauer et al. introduced an influential framework for monitoring Linear Temporal Logic (LTL) properties based on a three-valued semantics: the formula is already satisfied by the given prefix, it is already violated, or it is still undetermined, i.e., it can still be satisfied and violated by appropriate extensions. However, a wide range of formulas are not monitorable under this approach, meaning that they have a prefix for which satisfaction and violation\nwill always remain undetermined no matter how it is extended. In particular, Bauer et al. report that 44% of the formulas they consider in their experiments fall into this category.\n\nRecently, a robust semantics for LTL was introduced to capture different degrees by which a property can be violated. In this paper we introduce a robust semantics for finite strings and show its potential in\nmonitoring: every formula considered by Bauer et al. is monitorable under our approach. Furthermore, we discuss which properties that come naturally in LTL monitoring - such as the realizability of all truth\nvalues - can be transferred to the robust setting. Lastly, we show that LTL formulas with robust semantics can be monitored by deterministic automata and report on a prototype implementation.\n\nJoint work with Corto Mascle, Daniel Neider, Maximilian Schwenger, Paulo\nTabuada and Alexander Weinert.\n\nhttps://www.csc.liv.ac.uk/research/seminars/abstract.php?id=695
LOCATION:
END:VEVENT
END:VCALENDAR