Pierre Wolper (Université de Liège), On the Use of Automata for Representing Arithmetic Constraints

This talk presents a survey of automata-based techniques for representing and manipulating linear arithmetic constraints. After introducing the basic concepts used in this approach, both representing integer constraints by finite-word automata and real constraints by infinite-word automata is discussed. Various results about the construction of automata from constraints and about the specific properties of automata representing arithmetic constraints are then presented. Finally, the problems of computing the limit of a sequence of arithmetic automata and of computing formulas from automata are briefly considered.