Item

Abstract

Set constraints are inclusions between expressions denoting sets of trees (over a given alphabet of constructor symbols). The efficiency of their satisfiability test is a central issue in set-based program analysis, their main application domain. We introduce the class of {\em set constraints with intersection}\/ (the only operators forming the expressions are constructors and intersection) and show that its satisfiability problem is DEXPTIME-complete. This is the first class of set constraints (over a general constructor alphabet) that falls into this complexity class. The solved form in our algorithm represents the least solution as a tree automaton and exhibits which variables denote the empty set. We furthermore prove that set constraints with intersection are equivalent to {\em definite set constraints}\/ (in expressive power, and the satisfiability problems are linearly inter-reducible). The class of definite set constraints was the first one for which the decidability question was solved; we hereby settle also the complexity question.