Bastien Maubert Master 2RI 2008-2009 on "Synchronizing automata and their applications to games with imperfect information".

 

Nicolas Bitouzé Master 2RI 2007-2008 on "Observability Problems for Diagnosis, Control, or Games with Imperfect Information", with Laurie Ricker.

 

Guillaume Feuillade from ENS Cachan (2002-2005) Defense 8 december 2005 at IRISA

Claude Jard, IRISA, ENS Cachan, (president)

Jean-Michel Couvreur, LIFO, Université d'Orléans (referee)

Ahmed Bouajjani LIAFA, Université Paris 7 (referee)

Wieslaw Zielonka, LIAFA, Université Denis Diderot

Serge Haddad, LAMSADE, Université Paris Dauphine

Sophie Pinchinat, IRISA, Université Rennes 1 (supervisor)

Title: Specifications Logiques de Réseaux de Petri.

Abstract : In practice, concurrent objects are preferred to sequential objects since for example, their realization onto distributed architectures is made easier, they bring high computational performances, etc. Automatic construction of concurrent models is then a challenging problem. This thesis investigates the synthesis (automated construction) of Petri nets from branching-time logical specifications.
Most of existing logical-based synthesis methods rely on word-automata or tree-automata to deliver a sequential object. Unfortunately extracting the concurrency inherent to the Petri models from the synthesized sequential modal is not always possible: the synthesized sequential model does not necessarily distribute properly. Then, existing algorithms do not apply in our concurrent setting anymore; incidentally decidability of this synthesis problem is an open question. This thesis first addresses decidability issues (when restricting either the class of specifications or the class of models), and second studies the narrow connections between formulas and Petri nets (e.g. logical statements for Petri net flows properties).
 

Stéphane Riedweg, Doctorant INRIA-Région (2000-2003) Defense 19 december 2003 at IRISA.

Michel Raynal, IRISA (president)

André Arnold, LaBRI (referee)

John Thistle, University of Waterloo (referee)

Paul Gastin, LIAFA

Philippe Darondeau, IRISA (supervisor)

Sophie Pinchinat, IRISA, Université Rennes 1 (substitute supervisor)

Title: Logiques pour le contrôle d'automatismes discrets.

Abstract (in French): Le contrôle de systèmes à évènements discrets est une problématique générale consistant à construire, de façon automatique, un contrôleur pour restreindre le comportement d'un système afin d'assurer un objectif fixé (non réaliser par le système). Dans le cadre des systèmes à évènements discrets (c'est à dire des systèmes dynamiques dont la réaction aux événements physiques est considérées comme atomique), différentes théories et constructions existent, suivant les différents objectifs de contrôle et les différentes contraintes pour le contrôle.
Je propose un cadre formel et unifié pour une large classe de problèmes de contrôle par l'utilisation des logiques temporelles. Ces logiques sont dédiées à l'origine à l'analyse et la vérification des systèmes à événements discrets. Pour les adapter au problème du contrôle, j'ai défini une extension de ces logiques, obtenue par ajout de quantificateurs dans les formules. En particulier, j'ai étudié une telle extension pour le mu-calcul, qui est la logique temporelle la plus générale. La logique résultante, le mu-calcul quantifié, se révèle être très expressive: elle offre un moyen simple et uniforme de décrire différents problèmes de contrôle. Les différents paramètres comme le type de système à contrôler, le type de contrôle à exercer, l'objectif de contrôle, le type d'interaction entre le contrôleur et le système ainsi que différents critères d'optimalité peuvent être considérés. On peut, par exemple, spécifier un contrôle maximum permissif, c'est à dire un contrôle contraignant le moins possible le système. La construction des contrôleurs est alors obtenue en utilisant les résultats de la théorie des automates d'arbres et de la théorie des jeux.
A ma connaissance, aucune autre approche existante ne permet de saisir un si vaste ensemble de concepts.
Enfin, un second volet de mes travaux étend les résultats précédents pour répondre au problème du contrôle de systèmes sous observation partielle, c'est à dire le contrôle de systèmes munis d'actions internes, non visibles par le contrôleur.

 

Mirabelle Nebut , Doctorant MESR (2000-2003), Co-encadrement avec P. Le Guernic (INRIA). Defense 19 november 2002 at IRISA.

Jean-Pierre Banâtre, IRISA (president)

Robert De Simone, INRIA Sophia(referee)

Paul Caspi, CNRS Grenoble (referee)

Ahmed Bouajjani, Université

Paul Le Guernic, IRISA (supervisor)

Sophie Pinchinat, IRISA, Université Rennes 1 (substitute supervisor)

Title: Réactions synchrones : spécification et analyse

Abstract (in French): L'approche synchrone est dédiée à la conception des systèmes réactifs. Grâce à leur sémantique forte, des langages synchrones comme Esterel, Lustre et Signal permettent de spécifier le comportement des systèmes de manière abstraite et rendent possible leur validation formelle, cruciale dans le contexte des applications critiques. La validation formelle des systèmes est un domaine de recherche en pleine expansion, spécialement en ce qui concerne les espaces d'état infinis et les aspects numériques. L'application de ces méthodes aux programmes synchrones est fondamentale, mais plus ou moins simple. Notamment dans le cas de Signal l'absence des variables est explicitée par une valeur spéciale, ce qui empêche l'interfaçage direct des outils Signal aux techniques existantes. Cette thèse traite de la manipulation de l'absencex des variables synchrones, plus particulièrement dans les langages flot de données. Après un état de l'art du traitement de l'absence dans les sémantiques et les analyses synchrones, on présente un langage d'horloges appelé CL, basé sur une extension par des aspects numériques des horloges booléennes utilisées dans le contexte de la compilation Signal. On montre que CL permet d'interfacer naturellement les modèles étendus avec l'absence explicite à des théories standard, de plusieurs manières.