Thèse de Doctorat de Guillaume Feuillade

English version of this page

Sujet

Spécification logique de réseaux de Petri

Résumé

Les objets concurrents présentent généralement des avantages pratiques sur les objets séquentiels : leur mise en oeuvre sur des architectures distribuées est plus aisée, il permettent de meilleures performances, etc. De fait, la construction automatique de modèles concurrents est un enjeu. Le sujet de cette thèse est l'étude des problèmes de synthèse de réseaux de Petri à partir de spécifications en logique du temps arborescent.
Les méthodes de synthèse à partir de spécifications logiques s'appuient généralement sur des automates de mots ou d'arbres pour générer des objets séquentiels. Obtenir un objet concurrent dans un second temps n'est pas toujours possible : en effet, le modèle séquentiel synthétisé lors de la première étape ne possède pas nécessairement les propriétés requises pour être distribuable. Par conséquent, les algorithmes existants ne s'appliquent pas dans notre cadre de synthèse d'objets concurrents ; la décidabilité du problème de synthèse est alors une question ouverte.

Sans intention de proposer un nouveau formalisme de spécification, nous étudions la synthèse de réseaux de Petri à partir de spécifications en logique temporelle, et plus généralement celui de la satisfiabilité d'une formule sur la classe des réseaux de Petri. Nous prenons comme point de départ la plus expressive des logiques du temps arborescent~: le Mu-calcul. Le fil conducteur est la recherche de la frontière de décidabilité pour le problème de satisfiabilité d'une formule sur la classe des réseaux de Petri ; nous proposons des restrictions successives de la logique pour approcher cette frontière. Cette étude s'accompagne de celle de l'expressivité de la logique quand elle est considérée uniquement sur la classe de système concurrent que sont les réseaux de Petri.

Nous montrons dans cette thèse qu'il est nécessaire de restreindre très fortement la logique pour rendre la synthèse décidable (MSR'05 et article soumis), et que des logiques pourtant faibles permettent d'obtenir l'expressivité des machines à compteurs lorsque ces logiques sont interprétées sur la classe des réseaux de Petri (article en préparation). Nous nous attachons également à dissocier le rapport entre la logique et la structure d'un réseau, du rapport entre la logique et l'initialisation du réseau.

Jury

Thèse soutenue le 8 décembre 2005 à l'IRISA devant le jury :

• Claude Jard, IRISA, ENS Cachan, (président)
• Jean-Michel Couvreur, LIFO, Université d'Orléans (rapporteur)
• Ahmed Bouajjani LIAFA, Université Paris 7 (rapporteur)
• Wieslaw Zielonka, LIAFA, Université Denis Diderot (examinateur)
• Serge Haddad, LAMSADE, Université Paris Dauphine (examinateur)
• Sophie Pinchinat, IRISA, Université Rennes 1 (encadrant)

Documents

Manuscrit de thèse (pdf en français), Transparents de soutenance (pdf en français)