Projet TOAST
Réunion du 21 mars 2007

Première réunion :

Cette réunion a eu lieu à la bibliothèque du LSV le mercredi 21 mars 2007 de 15h à 16h30.

Participants :

SATIE : Mohamed Abbas-Turki, Jean-Pierre Barbot, Stéphanie Bay, Ana Lúcia Franco Driemeyer, Benoît Geller, Marc Jungers.

LSV : Thomas Brihaye, François Laroussinie, Nicolas Markey, Ghassan Oreiby.

Compte-rendu de la réunion :

• Marc présente le problème sur lequel porte notre projet : le cadre général est le domaine des télécommunications (par exemple téléphonie sans fil, ADSL, ...). Dans ce domaine, les interférences nuisent à la qualité de la communications. Ces interférences sont directement liées à la puissance d'émission des différents utilisateurs. Lorsque ces interférences sont élevées, une solution individualiste pour un émetteur consiste à augmenter la puissance d'émission. Cela n'est cependant pas dans l'intérêt général, puisque cela augmente les interférences pour les autres utilisateurs, qui vont à leur tour augmenter leur puissance d'émission.

  Cela conduit naturellement à un équilibre, que nous aimerions étudier au cours de ce projet. Marc a ensuite développé quelques aspects plus théoriques de ce problèmes, qui sont expliqués dans la note qu'il a rédigée.

• Nicolas a ensuite expliqué comment les activités du LSV peuvent s'appliquer à l'étude de ce problème. Une première simplification, grossière mais permettant d'arriver assez simplement à de premiers résultats, consiste à ne considérer qu'une bande de fréquences, et de discrétiser les puissances d'émission des utilisateurs du réseau. Ces utilisateurs peuvent alors augmenter ou diminuer leurs puissance d'émission dans ce modèle.

  Pour l'instant, dans le domaine de la vérification, très peu de travaux se sont intéressé aux problèmes d'équlibres. Les problèmes étudiés sont plus souvent des questions d'accessibilité, de sûreté, ou la vérification de propriétés exprimées dans la logique ATL. Aucun de ces formalismes ne permet d'exprimer des propriétés d'équilibre. Cependant, on peut ajouter dans notre modèle simplifié des stratégies pré-établies pour deux utilisateurs du réseau, et vérifier si ces stratégies permettent d'accueillir un troisième utilisateur sans pour autant permettre à ce nouvel utilisateur de couper les connexions des deux autres (une connexion est coupée si le rapport signal/bruit descend sous une valeur minimale).

  Cette première idée va être étudiée plus en profondeur avec l'outil Uppaal TiGa.

À propos du LSV