M2 Internship

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