IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Charlas Invitadas > 2021 > Monitor-Triggered Temporal Logic
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Gerardo Schneider

miércoles 3 de noviembre de 2021

11:00am Meeting room 302 & Zoom3 https://zoom.us/j/3911012202 (pass: s3)

Gerardo Schneider, Research Professor, University of Gothenburg, Sweden

Monitor-Triggered Temporal Logic

Abstract:

This talk is concerned with the combination of monitoring techniques and reactive synthesis based on temporal logic (LTL). We explore an approach that combines synthesis of declarative specifications in the presence of an existing behaviour model as a monitor, with the benefit of not having to reason about the state space of the monitor. We suggest a formal language (Monitor-Triggered Temporal Logic) with automata monitors as non-repeating and repeating triggers for LTL formulas. We use symbolic automata with memory as triggers, resulting in a strictly more expressive and succinct language than existing regular expression triggers. We give a compositional synthesis procedure for this language, where reasoning about the monitor state space is minimal. We show its applicability to specifications requiring counting and constraints over arbitrarily long sequence of events, where we can also see the power of parametrisation, easily handled in our approach. This is a joint work with Shaun Azzopardi and Nir Piterman, based on the paper “Incorporating Monitors in Reactive Synthesis without Paying the Price” recently presented at ATVA'21.