Abstract FR:

Cette these est consacree a l'etude d'une extension de la programmation concurrente avec contraintes fondee sur la logique lineaire. Le langage (lcc) qui en resulte permet de programmer des solveurs de contraintes complexes susceptibles de s'appuyer sur des structures de donnees evoluant de maniere non-monotone au cours du calcul. Lcc s'affranchit de la restriction des calculs a l'accumulation monotone d'information dans le store en axiomatisant les systemes de contraintes en logique lineaire et en autorisant la consommation des contraintes par les agents. Nous montrons que l'utilisation de contraintes consommables dediees au controle permet, via le codage d'etats dans le store, de specifier des strategies de propagation plus fines que ce que la programmation declarative des langages traditionnels de programmation par contraintes autorise. Nous montrons egalement que le langage des agents lcc est equivalent au langage utilise pour specifier le mecanisme d'inference des systemes de contraintes sous-jacents. Ce resultat, en effacant la frontiere entre langage-hote et solveur de contraintes, ouvre la voie une forme de programmation modulaire de solveurs. L'expressivite du cadre lcc est illustree par deux exemples de programmation de solveurs de contraintes par strates de complexite croissante, sur les domaines finis et sur les reels. Nous proposons notamment une reconstruction rationnelle d'un solveur de contraintes sur les reels, dans laquelle un algorithme de resolution fonde sur la methode du simplex est defini au-dessus d'un systeme de contraintes generique permettant la manipulation d'equations et d'inequations lineaires.