VOLUMÉTRIE POUR LES EXPRESSIONS RÉGULIÈRES TEMPORISÉS ET APPLICATIONS // VOLUMETRY FOR TIMED REGULAR EXPRESSIONS

Les automates temporisés ont été introduits en 1990, dans le contexte de la vérification des modèles temps-réel. Un des théorèmes les plus importants pour les automates est le théorème de Kleene qui établit l'équivalence entre langages reconnus par des automates et ceux décrits par des expressions régulières. En 1997, Asarin, Caspi et Maler ont définit les expressions régulières temporisés (TRE) et ont montré une version temporisés du théorème de Kleene. Ces expression régulières temporisées ont depuis récemment été utilisées comme spécifications pour les comportements des systèmes cyber-physiques.
Dans cette thèse nous souhaitons étudier les expressions régulières temporisés et leurs langages en utilisant/adaptant/créant plusieurs outils théoriques. Cette étude visant à établir de nouveaux résultats fondementaux pour les langages temporisés sera accompagnée d'une démarche plus algorithmique. En particulier nous envisageons la validation statistique des systèmes cyber-physiques par générations aléatoires de traces satisfaisant une spécification donnée sous forme de TRE.
Avec une approche langage formel, le premier objectif est de caractériser une sous-classes d'expression qui correspondrait aux automates temporisés déterministes. Une telle sous-classe serait close pour la complémentation des langages, une bonne propriété dont les langages temporisés généraux (non-déterministes) ne jouissent pas.
Avec une approche géométrique, les langages temporisés peuvent être vus comme des collections de polytopes bien particuliers.
Une approche précédente pour les automates temporisés permettait de calculer les volumes à l'aide d'équations fonctionnelles faisant intervenir des intégrales. Le deuxième objectif de la thèse est de comprendre comment calculer les volumes directement à partir d'une expression régulière temporisée par induction sur l'expression. Les polytopes associés aux langages temporisés peuvent se décomposer en une union de simplexes tous isométriques. Nous pensons qu'il est possible de caractériser le volume de tels polytopes par le comptage du nombre de simplexes qui le composent. Ainsi le calcul du volume pourrait se faire par une approche purement discrète où les sommations discrètes remplaceraient les intégrales. Il serait alors possible d'appliquer des méthodes de combinatoire énumérative de comptage de structures discrètes. Ces méthodes sont intimement liées aux méthodes de générations aléatoires uniformes.
Un outil théorique très utilisé dans différents domaines des mathématiques et de l'informatique est l'utilisation de fonctions génératrices (ceci est particulièrement vrai en théorie des automates pour les expressions régulières).
Le troisième objectif de la thèse sera donc d'établir des méthodes de calculs pour différents types de fonctions génératrices que l'on associera aux TRE.
Le calcul de ces fonctions devraient permettre de généraliser aux TRE les générateurs aléatoires de Boltzmann qui sont les générateurs les plus efficaces
pour générer aléatoirement et uniformément des structures combinatoires de très grandes tailles (appartenant par exemple à des ensemble de permutations, d'arbres, de graphes...).
Pour résumé, les trois objectifs théoriques de la thèse sont:
- Caractérisation du déterminisme et d'autres bonnes sous-classes d'expressions régulières temporisées,
- Etablissement et étude du lien continu/discret entre volume de polytopes et comptage de simplexes inclus, pour les polytopes des langages temporisés,
- Définition/caractérisation et calcul de différents types de fonctions génératrices associées aux TRE,
- Applications à la génération aléatoire de mots temporisés de grandes tailles à l'aide de générateurs de Boltzmann adaptés au TRE. Ce travail s'accompagnera d'applications obtenus
- par le développement d'un générateur aléatoire de mots temporisés,
- par l'utilisation de ce générateur dans le contexte de validation statistique des systèmes cyber-physiques.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Timed automata have been introduced in 1990 in the context of the verification of real-time systems. One of the most important theorems of automata theory is the Kleene Theorem stating the equivalence between the languages recognised by automata and those described by regular expressions.
In 1997, Asarin, Caspi et Maler defined the timed regular expressions (TRE) and showed a timed version of the Kleene Theorem. These timed regular expressions has recently been used as specification in the context of monitoring of cyber-physical system traces via 'timed pattern matching'.
In this thesis we would like to study timed regular expressions and their languages by using/adapting/creating several theoretical tools. In paralell of this study that aims at establishing new fundamental results for timed languages, the PhD student will design and implement algorithms that will be applied for the validation of cyber-physical systems by random generation of traces satisfying a specification given as a TRE.
With a formal language approach, an objective of the thesis will be to characterise a sub-class of expressions that would correspond to deterministic timed automata. Such a sub-class would be closed under complementation of languages, a good property that the general timed languages do not enjoy.
On the other hand, with a geometric approach, the timed languages can be viewed as collections of polytopes with some special properties. A previous work for timed automata enables one to compute volumes via defining them through functional equations involving integrals. A second goal of the thesis is thus to understand how one could compute the volume directly from a TRE by induction on the expression. The polytopes associated to the language can be decomposed into a union of simplexes all isometric. We think that it could be possible to characterise the volume of such polytopes by counting the number of simplices that compose them. Thus the computation of the volume could be done in a purely discrete approach where discrete summations would replace integrals. It would be then possible to apply methods from enumerative combinatorics to count discrete structures. These methods are tightly linked to uniform random sampling methods.
Finally, a theoretical tool extensively used in different fields of mathematics and computer science is the use of generating functions (this is particularly true in automata theory for regular expresions). The third goal of the thesis will be to establish methods to compute several types of generating functions that will be associated to TRE. The computation of these functions should allow us to lift to the timed world Boltzmann samplers that are the most efficient tool to sample uniformly very large combinatorial structures (belonging e.g. to sets of permutaitons, trees, graphs,...).
To sum up, the different goals of the thesis are
- Characterization of determinism and other good sub-classes of timed regular expressions,
- Establishment and study of the link continuous/discrete between volumes of polytopes and counting of simplexes included in them (for polytopes of timed languages),
- Definition, characterization and computation of several types of generating functions associated to TRE,
- Applications to the random sampling of large timed words using Boltzmann samplers adapted to TRE.
This theoretical work will come with application obtained
- via the programming of random samplers of timed words
- via the use of these generators in the context of statistical validation of cyber-physical systems.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Début de la thèse : 01/10/2025

Concours allocations

Université Grenoble Alpes

217 MSTII - Mathématiques, Sciences et technologies de l'information, Informatique

Excellent baggage théorique en mathématique et/ou informatique théorique, compétences avancées en programmation
strong background in mathematics and/or theoretical computer science, advanced programming skills.