• Langue : Français
• Discipline : Informatique
• Identifiant : Inconnu
• Type de thèse : Doctorat
• Date de soutenance : 01/01/1998

Résumé en langue originale

Les contraintes ensemblistes permettent d'exprimer des relations entre des ensembles d'arbres finis. Syntaxiquement, elles consistent en des inclusions ou des non-inclusions entre des expressions ensemblistes comportant les operateurs usuels de la theorie de ensembles, comme l'union, l'intersection, le complementaire, mais egalement la composition fonctionnelle et des operateurs de projections. L'un des domaines d'application de ces contraintes est l'analyse de programmes, connu sous le nom d'analyse ensembliste. Dans ce travail, nous nous interessons a deux classes de contraintes introduites pour ces motivations : la classe definie proposee par heintze et jaffar et la classe co-definie par charatonik et podelski. Nous proposons pour chacune d'elles une extension. Celles-ci consistent a ajouter des descriptions intensionnelles sous la forme de formules positives monadiques. Ces classes sont alors dites generalisees. Pour la classe definie generalisee (interpretee sur les ensembles d'arbres finis) un algorithme repondant au probleme de satisfiabilite est presente. Celui-ci, base sur les automates d'arbres, donne pour un systeme satisfiable une representation de la plus petite solution. Cet algorithme donne egalement un test de satisfiabilite pour la classe co-definie generalisee (interpretee sur les ensembles d'arbres finis), puisqu'elle se revele etre la duale par complementation de celle definie generalisee. Nous nous interessons alors a la classe co-definie generalisee, mais interpretee sur les ensembles d'arbres finis ou infinis. Nous proposons pour celle-ci un algorithme pour la satisfiabilite utilisant egalement des automates d'arbres et calculant pour un systeme satisfiable la plus grande solution de celui-ci.