formation par la recherche / formation doctorale / enseignement, stages / sujets de thèses

Logiques pour le contrôle d'automatismes discrets

Localisation :Irisa, Rennes

Equipe Ep-Atr

Responsable : Sophie Pinchinat (tél: 02-99-84-72-54, email: pinchina@irisa.fr)

Mot-clés : systèmes à évènements discrets, synthèse de contrôleur, logiques modales. Financement : A déterminer.

Sujet : De nos jours, des systèmes de plus en plus complexes sont mis en oeuvre dans de nombreux domaines (systèmes de production, systèmes informatiques, systèmes de transport, systèmes administratifs,...). La complexité de ces systèmes peut être liée d'une part à leur taille (nombre d'éléments du système), et d'autre part à leur fonctionnement (type et nombre des interactions entre les éléments du système). Les principaux problèmes que posent les systèmes complexes sont la compréhension et/ou la validation de leur fonctionnement, leur dimensionnement, etc.

Le cas particulier des problèmes de validation des systèmes trop complexes pour être traités ``manuellement'' est à l'origine depuis une vingtaine d'années d'un développement spectaculaire de méthodes formelles souvent automatisées (e.g. model-checking, démonstration automatique, synthèse, simulation, test, etc). L'approche par synthèse d'automatismes discrets consiste à construire automatiquement un contrôleur du système qui garantit a priori les bonnes propriétés du système contrôlé. La méthode de construction est guidée par un objectif de contrôle qui exprime les propriétés attendues du système contrôlé.

L'objectif de cette thèse est d'étudier, sur un plan théorique dans un premier temps, des modèles de systèmes et des logiques bien adaptées à la spécification d'objectifs de contrôle. En particulier, la décidabilité de ces logiques, ainsi que la complexité du problème de décision devra être traitée. Ensuite, si de telles logiques peuvent permettre d'énoncer (et de vérifier automatiquement) l'existence d'une solution au problème du contrôle, il n'en reste pas moins la question de synthétiser un contrôle. Dans ce deuxième volet, un enrichissement des algorithmes de décision des logiques pourront par exemple servir de point de départ. Ce sujet s'inscrit dans une grande famille de travaux pour lesquels divers résultats ont déjà été proposés. Toutefois, la problématique énoncée offre encore un très large spectre d'études à mener (e.g. modèles de théorie des jeux et logiques modales, etc.).