M2 Internship

Timed distances and approximate verification of timed systems

Supervisors: Eugene Asarin and Aldric Degorre

Location: IRIF (Paris)

Context: This internship is related to two recent ANR projects CyPhAI (Franco-Japanese) and MAVERIQ, PhD thesis available.

Cyber-physical systems (such as autonomous cars, medical equipment etc.) combine non-trivial discrete and continuous behaviors. Their runs can be observed as timed words – sequences of discrete events and continuous time durations, for example

a 1.234 b 3.141 a 2.71828 a 0.0001 b.

sets of such words (timed languages) are recognized by timed automata. These concepts are studied since 1990s, they are extensively applied to modelling and verification.

It is clear, that in practice behaviors are observed with some finite precision with some small error, and verification of systems should take into account this error, to be on the safe side. A key to such an analysis is a relevant distance between timed words,

Recently, we have introduced a new distance on timed words, with nice mathematical properties and practically plausible.We have also stated some natural approximate verification problems with a finite precision with respect to our distance, and analysed their complexity. This work will be the starting point for the internship.

Some of the following questions will be addressed:

geometric and topological properties of the new distance
other distances corresponding to various kinds of systems and observations
formulation approximated model-checking and monitoring of timed with respect to those distances
algorithms for approximated model-checking and monitoring
implementation thereof

Basic knowledge of automata, algorithmics, topology, and taste for fundamental informatics are mandatory, as well as programming skills. The ideal candidate should know basics of model-checking (e.g. course 1-22 of MPRI), and of timed automata/languages (e.g. course 2-8-2).