BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//labri.fr//NONSGML kigkonsult.se iCalcreator 2.41.92//
CALSCALE:GREGORIAN
METHOD:PUBLISH
UID:dc167d5a-ddc2-4de0-b361-bea04b05ed6e
X-WR-CALNAME:[MTV] Léo Exibard - Runtime monitoring for Hennessy-Milner log
 ic with recursion over systems with data
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
TZUNTIL:20260329T010000Z
BEGIN:STANDARD
TZNAME:CET
DTSTART:20231029T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RDATE:20241027T030000
RDATE:20251026T030000
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20240331T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RDATE:20250330T020000
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:dc167d5a-ddc2-4de0-b361-bea04b05ed6e
DTSTAMP:20260425T182319Z
CLASS:PUBLIC
DESCRIPTION:Runtime verification consists in checking whether a program sat
 isfies a given specification by observing the trace it produces during its
  execution. In the regular setting\, Hennessy-Milner logic with recursion 
 (recHML)\, a variant of the modal $\mu$-calculus\, provides a versatile ba
 ck-end for expressing linear- and branching-time specifications. In this t
 alk\, I will discuss an extension of this logic that allows to express pro
 perties over data values (i.e. values from an infinite domain) and examine
  which fragments can be verified at runtime. Data values are manipulated t
 hrough equality tests in modalities and through first-order quantification
  outside of them. They can also be stored using parameterised recursion va
 riables.\n\nI then examine what kind of properties can be monitored at run
 time\, depending on the monitor model. A key aspect is that the logic has 
 close links with register automata with non-deterministic reassignment\, w
 hich yields a monitor synthesis algorithm\, and allows to derive impossibi
 lity results. In particular\, contrary to the regular case\, restricting t
 o deterministic monitors strictly reduces the set of monitorable propertie
 s.\n\nI then conclude by examining whether we can delineate a maximally mo
 nitorable fragment for the logic\, and the picture turns out to be quite i
 ntriguing.\n\nThis is joint work with the MoVeMnt team (Reykjavik Universi
 ty): Luca Aceto\, Antonis Achilleos\, Duncan Paul Attard\, Adrian Francala
 nza\, Karoliina Lehtinen.
DTSTART;TZID=Europe/Paris:20240528T140000
DTEND;TZID=Europe/Paris:20240528T150000
LOCATION:salle 178\, zoom: https://bordeaux-inp-fr.zoom.us/j/89508306159
SEQUENCE:0
SUMMARY:[MTV] Léo Exibard - Runtime monitoring for Hennessy-Milner logic wi
 th recursion over systems with data
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR
