Solving Co-definite Set Constraints with Membership Expressions over Sets of finite Trees

Recently, W. Charatonik and A. Podelski have introduced the class of
co-definite set constraints (dual of the class of definite set
constraints proposed by Heintze and Jaffar in 1990). This class is
defined as inclusions of the form se \subset se', where se is built
with variables, unary function symbols and constants and se' is a
general set expressions without complementation. Those constraints can
be interpreted over either sets of finite trees or sets of finite and
infinite trees. Charatonik and Podelski have shown that a system of
such constraints (whether it is satisfiable) has a greatest solution
and proved the DEXPTIME-completeness for the satisfiability problem.

We improve this class by adding a set operation, called membership
expression, in the right-hand side of constraints. Such membership
expressions look like:

{ x | \exists y1,...,yn: s1 \in Exp1 and ... and sm \in Expm }

where x,y1,...,yn are first-order variables, s1,...,sm are first-order
terms and Exp1,...,Expm are set expressions.

As done for other classes of set constraints, we use a tree automata
approach for solving the satisfiability problem of this class. It
turns out that this improvement changes neither the complexity for
this problem nor the "greatest solution" property.