Solving systems of set constraints using tree automata

Abstract

A set constraint is of the form (formula presented) where exp1 and exp2 are set expressions constructed using variables, function symbols, and the set union, intersection and complement symbols. An algorithm for solving such systems of set constraints was proposed by Aiken and Wimmers [1], We present a new algorithm for solving this problem. Indeed, we define a new class of tree automata called Tree Set Automata. We prove that, given a system of set constraints, we can associate a tree set automaton such that the set of tuples of tree languages recognized by this automaton is the set of tuples of solutions of the system. We also prove the converse property. Furthermore, if the system has a solution, we prove, in a constructive way, that there is a regular solution (i.e. a tuple of regular tree languages) and a minimal solution and a maximal solution which are actually regular.