Room 206 (2nd floor, badged access)
7 July 2023 - 10h00
Parametric timed formalisms for specification and monitoring (PhD defense) (Phd Defense)
by Akshay Mambakam from VERIMAG, Université Grenoble Alpes
Abstract: PhD Defense Friday/7th of July 2023/Room 206, VERIMAG, IMAG Building, 700 Av. Centrale, 38400 Saint-Martin-d'Hères
Title: Parametric timed formalisms for specification and monitoring (PhD defense)
By Akshay Mambakam, VERIMAG, Université Grenoble Alpes
Supervised by Nicolas Basset (UGA, VERIMAG), Thao Dang (CNRS, VERIMAG)
Cyber-Physical Systems (CPS) like smart power grids, autonomous cars, and robots are finding numerous applications. Data generated from these systems can be used to detect faults, calculate metrics and diagnostics. We concentrate on describing and detecting aspects of behaviours that deal with time. For example, power outages of more than a specified duration or abnormality in heart beats for many consecutive pulses for a long time. Timed formalisms such as Signal Temporal Logic (STL) and Timed Regular Expressions (TRE) allow rigorous monitoring of such behaviours of CPS systems.
In the first part of this thesis presentation, we explain a parametric version of STL and show how to use it to learn to predict behaviours almost as accurately as experts. This involves identification of parameters that generate accurate predictors. The accuracy of these predictors is decided with respect to given bounds on false positives and false negatives. We then explain our algorithm for the task of parametric identification which is based on queries and exploits monotonicity. We demonstrate our method by characterizing Electrocardiogram (ECG) signals using parametric specifications.
The second part is concerned with parametric TRE which are regular expressions augmented with duration constraints and parameters. We introduce and explain three type of parametric TRE with the aid of examples. Regular expressions can be efficiently used to detect patterns in text. Inspired by this, we introduce the theory and application of parametric TRE for detecting patterns in time-series data. We finish by defining and solving the problem of parametric identification for TRE.
Keywords: Parametric Signal Temporal Logic, Parametric Timed Regular Expressions, Monitoring, Parametric identification
Jury:
Étienne André, Rapporteur, Université Sorbonne Paris Nord
Ezio Bartocci, Rapporteur, TU Wien
Saddek Bensalem, Université Grenoble Alpes
Patricia Bouyer-Decitre, CNRS, Director of LMF (Laboratoire Méthodes Formelles)
Dejan Ničković, Austrian Institute of Technology
Nicola Paoletti, King's College London
Thao Dang, Directrice de thèse, CNRS
