Programmation par contraintes sur les flux de données
Institution:
CaenDisciplines:
Directors:
Abstract EN:
In this thesis, we investigate the generalisation of constraint programming on finite variables to stream variables. First, the concepts of streams, infinite sequences and infinite words have been extensively studied in the litterature, and we propose a state of the art that covers language theory, classical and temporal logics, as well as the numerous formalisms that are strongly related to those. The comparison with temporal logics is a first step towards the unification of formalisms over streams, and because the temporal logics are themselves numerous, the classification of these allows the extrapolation of our contributions to other contexts. The second goal involves identifying the features of the existing formalisms that lend themselve to the techniques of constraint programming over finite variables. Compared to the expressivity of temporal logics, that of our formalism is more limited. This stems from the fact that constraint programming allows only the conjunction of constraints, and requires encapsulating disjunction into constraint propagators. Nevertheless, our formalism allows a gain in concision and the reuse of the concept of propagator in a temporal setting. The question of the generalisation of these results to more expressive logics is left open.
Abstract FR:
Dans ce manuscrit, nous étudions la généralisation de la programmation par contraintes sur les variables à domaines finies aux variables flux. D'une part, les concepts de flux, de séquences infinies et de mots infinies ont fait l'objet de nombreux travaux, et un objectif consiste à réaliser un état de l'art qui couvre la théorie des langages, les logiques classiques et temporelles, ainsi que les nombreux formalismes qui sont fortement apparentés à ceux-ci. Le rapprochement effectué avec les logique temporelles est un premier pas vers l'unification des formalismes sur les flux, et les logiques temporelles étant elles-même nombreuses, nous établissons une classification de celles-ci qui permettra l'extrapolation des contributions à d'autres contextes. Le second objectif consiste à identifier les éléments de ces formalismes qui permettent le traitement des problèmes de satisfactions avec les techniques de la programmation par contraintes sur les variables à domaines finis. Comparée à l'expressivité des logiques temporelles, celle de notre formalisme est plus limitée. Ceci est dû au fait que la programmation par contraintes ne permet que la conjonction de contraintes, et impose d'intégrer la disjonction dans la notion de propagateur de contraintes. Notre formalisme permet un gain en concision et la réutilisation de la notion de propagateur. La question de la généralisation à des logiques plus expressives est laissée ouverte.