next up previous
Up: Sujets de thèse autour Previous: Sujet : Techniques de

Sujet : L(A)=L(B)?

 

Fiche signalétique

Responsable Paul-Yves Gloess 05 56 84 69 27 Paul.Gloess@labri.u-bordeaux.fr
Collaborateurs Pierre Castéran 05 56 84 69 31 Pierre.Casteran@labri.u-bordeaux.fr
Géraud Sénizergues 05 56 84 60 48 ges@labri.u-bordeaux.fr
Equipe Programmation symbolique
Titre
L(A)=L(B)?
Catégorie Théorique
Position/AltaRica Outil satellite d'une version ultérieure
Prospectif
Financement Bourse de thèse MENRT

Présentation du sujet

Objectifs

L'objectif essentiel de la thèse est d'obtenir une version "mécanisée" de la preuve du théorème de Géraud Sénizergues: "L(A)=L(B) est décidable, A et B étant des automates à pile finis déterministes", sous une forme convaincante pour le mathématicien ou le théoricien de l'informatique. Il faut noter l'importance du résultat obtenu par Géraud Sénizergues, résultat qui fut pendant longtemps une conjecture intéressant la communauté scientifique internationale. Au delà de cet objectif, qui constitue en lui même un véritable "challenge", on s'efforcera d'abstraire les principes généraux de la preuve, sous la forme d'une bibliothèque de théories et de stratégies de preuve applicables à d'autres résultats de décidabilité.

Contexte

La preuve rédigée par Géraud Sénizergues dans ~ges/public_html/lalb_l.ps (version améliorée du rapport LaBRI RR-1161-97) compte 84 pages de texte, jusqu'au résultat principal, le Théorème 9.3, qui énonce la décidabilité du problème d'équivalence, pour des automates à pile finis déterministes. Le texte est dense, et les preuves des différents lemmes non triviales, mais il est relativement auto-suffisant: les objets mathématiques du domaine sont pour la plupart définis; les théorèmes extérieurs au texte sont en petit nombre: ce sont des résultats classiques dont les preuves sont facilement accessibles dans les livres. Cet aspect, renforcé par la présence au LaBRI de l'auteur de la preuve, rend l'entreprise de mécanisation envisageable, au moyen d'assistants de preuves internationalement reconnus tels que PVS (SRI International) ou Coq (INRIA) disponibles au LaBRI.

Démarche et travail demandé

Il ne s'agit pas uniquement d'obtenir une preuve du Théorème 9.3 au moyen de PVS ou Coq. Encore faut-il que le théoricien (tel que l'auteur de la preuve) et le praticien (utilisateur de PVS ou Coq) puissent être convaincus du bien-fondé de la preuve mécanique, et de l'identité du résultat mécaniquement démontré avec le Théorème 9.3. Cette exigence implique en particulier qu'aucun axiome ne soit introduit, pour pallier la preuve de résultats extérieurs utilisés, et que les définitions des notions sous-jacentes (par exemple, les automates à pile, la décidabilité) soient présentées sous une forme accessible et indiscutable au théoricien.

En pratique, on aura intérêt à suivre de près la preuve humaine, sous peine de la réinventer, ce qui pourrait prendre beaucoup plus de temps, et n'est pas demandé. D'autre part, dans une perspective de réutilisabilité des théories PVS ou Coq, et plus généralement d'intéressement du théoricien aux résultats de la thèse, il est impératif d'établir une correspondance limpide entre le texte initial et la version mécanisée.

Bien que le résultat principal soit un résultat de décidabilité, de nombreux lemmes utilisent des preuves non constructives, de sorte que le choix du meilleur outil n'est pas évident. L'impact des différences entre les logiques de PVS et Coq, sur la faisabilité de l'entreprise, devra être finement analysé avant de prendre une décision. Certaines de ces différences sont majeures: distinction existant en Coq (pas en PVS) entre les sortes Set et Prop; notion d'égalité; typage décidable en Coq et indécidable en PVS. Elles ont un impact sur le langage des fonctions récursives, et la nature des preuves. D'autres différences plus mineures peuvent néanmoins prendre de l'importance en pratique, étant donné l'ampleur du domaine à traiter: surcharge possible en PVS, pas en Coq; currification implicite en Coq, identification des types [D1, ..., Dn -> D] et [[D1, ..., Dn] -> D] en PVS.

On comparera dans une première phase de quelques mois d'expérimentation les deux logiques sur un échantillon représentatif du texte de Géraud Sénizergues, incluant en particulier l'échantillon abordé par une étude préliminaire de faisabilité sous PVS (~gloess/pvs/ges/README). Le choix de l'outil reposera sur une confrontation des résultats de cette comparaison avec les objectifs énoncés plus haut. La confiance que l'on peut avoir dans l'outil lui-même est liée à la conception de celui-ci: c'est un aspect à ne pas négliger.

On achèvera dans une seconde phase la formalisation et les preuves, jusqu'au Théorème 9.3, à l'aide de l'outil choisi.

La troisième phase visera l'objectif de réutilisabilité.


next up previous
Up: Sujets de thèse autour Previous: Sujet : Techniques de

Equipe Modélisation, Vérification et Test des systèmes informatisés
Fri May 15 10:32:44 CEST 1998