Help Privacy Policy Disclaimer
  Advanced SearchBrowse




Journal Article

Set Constraints with Intersection


Charatonik,  Witold
Programming Logics, MPI for Informatics, Max Planck Society;


Podelski,  Andreas
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available

Charatonik, W., & Podelski, A. (2002). Set Constraints with Intersection. Information and Computation, 179, 213-229.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-3070-7
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.