Laboratoire : LIAFA, équipe Verif
Responsables : Eugene Asarin (Prof. P7), Mihaela Sighireanu (MdC P7)
Contacts : asarin@liafa.jussieu.fr, sighirea@liafa.jussieu.fr
Les langages temporisés (étudiés depuis une quinzaine d’années) représentent les comportements de systèmes pour lesquels non seulement l'ordre d'événements, mais aussi les intervalles de temps entre ces événements sont importants. Un ensemble de comportements temporisés (langage), à la différence d’un langage classique, n’est plus un ensemble discret, il a une certaine « épaisseur », peut être vu comme une union des sous-ensembles de Rn, et il est naturel de mesurer leur volume. On croit que ce volume est une caractéristique importante d’un langage temporisé.
Le but de ce stage est d’étudier plusieurs aspects de cette notion de volume et ses applications éventuelles parmi les suivantes :
· Comment définir la notion de volume V pour un langage de mots temporisés de longueur fixe ? Comment calculer ce volume ?
· Etant donné un langage de mots temporisés infinis, pour chaque longueur n on peut tronquer les mots après n transitions et mesurer le volume V(n) du langage de mots finis ainsi obtenu. On croit que le comportement asymptotique est une caractéristique importante de la « taille », « robustesse » du langage. Comment définir correctement V(n) ? Comment calculer son comportement asymptotique ?
· Est-ce que V et V(n) sont des bonnes mesures pour les langages ? Comment elles se comparent avec d’autres mesures quantitatives ?
· Application 1. Quand on fait la vérification des propriétés de sûreté des systèmes temporisé, l’outil de vérification peut fournir un chemin qui mène vers une erreur. Comment calculer le volume d’un tel chemin ? Comment « gonfler » un chemin pour augmenter son volume ? Comment trouver le chemin le plus volumineux ? Est-ce que vraiment les chemins volumineux sont plus dangereux ?
· Application 2. Quand on utilise les automates et les langages temporisés pour la planification et l’ordonnancement, il semble que les plans plus volumineux sont meilleurs, plus faciles à réaliser, plus souples. Appliquer les volumes à la comparaison de plans, amélioration de plans, recherche d’un meilleur plan.
En fonction de l’avancement du stage et des goûts du stagiaire l’accent sera mis sur certains parmi les points énumérés ci-dessus. Si l’approche s’avère fructueuse, le stage peut être continué par une thèse.
Il serait préférable pour le candidat d’avoir suivi le cours sur la vérification des automates temporisés (2-8). Autres cours qui peuvent être utiles : 2-9, 2-16, 2-14. Certaines connaissances en algèbre linéaire et géométrie (niveau Bac+2) seront utilisés lors de stage.