Sujet : Logique de Presburger sur les réels et langages rationnels de mots finis

Responsable : André Arnold, Jean-Michel Couvreur
Téléphone : 05 40 00 60 94, 01 47 40 75 38
e-mail : arnold@labri.fr, couvreur@labri.fr
Site Web : http://www.labri.fr
Equipe : MVTsi

Présentation du sujet :

Les contraintes numériques linéaires sont des structures élémentaires utilisées dans de nombreux domaines de l'informatique et d'autres disciplines. Elles abondent dans des algorithmes et des outils pour résoudre des problèmes de décision et d'optimisation. Le pouvoir d'expression des contraintes peut être largement étendu en les plongeant dans une théorie du premier ordre par l'introduction d'opérateurs booléens et de quantificateurs. Ces théories correspondent aux logiques de Presburger sur N, Z, Q et R. Une solution élégante pour traiter ces formules est l'utilisation d'automates de mots finis ou infinis. Le principe consiste à coder en binaire un vecteur d'entiers par un mot fini, les solutions d'une formule par un automate et de transposer les opérateurs de la logique par des opérations sur les automates ; de manière analogue, on traite des variables réelles en utilisant des automates sur des mots infinis. Cette méthode introduite par Büchi en 1960 connaît de nos jours un succès grandissant et est au coeur de la conception de nouveaux outils essentiels pour l'étude des systèmes infinis [BW02].

Le point de départ de ce sujet repose sur une idée simple : une formule de Presburger sur les réels est caractérisée par ses solutions rationnelles, c-a-d les solutions codées par des mots infinis ultimement périodiques, et un mot ultimement périodique peut être codé par une paire de mots finis (un préfixe, une période) ou plus simplement par un mot fini en utilisant un caractère spécial. Cette remarque pose plusieurs questions :

Un premier élément de réponse sur la rationalité de l'ensemble des solutions se trouve dans [CNP94]. L'objectif de cette thèse est : (1) de développer une procédure de décision pour les formules de Presburger sur les réels basée sur le codage préfixe-période ; (2) de faire le lien avec d'autres structures décidables ; (3) d'appliquer ces résultats à la vérification de systèmes infinis.

Mot-clés : arithmétique, logique, vérification, systèmes infinis

Références :

[BW02] B. Boigelot, P. Wolper. Representing Arithmetic Constaints with finite Automata: An overview. Proc. International Conference on Logic Programming, LNCS, volume 2401, pages 1--19, 2002.

[CNP94] H. Calbrix, M. Nivat, A. Podelski. Sur les mots ultimement périodiques des langages rationnels de mots infinis. Comptes Rendus de l'Académie des Sciences, Paris, Série I, volume 318 , pages 493--497. 1994.