Logic in Computer Science (LICS 1997)

Paper: Set constraints with intersection (at LICS 1997)

Authors: Witold Charatonik Andreas Podelski

Abstract

Set constraints are inclusions between expressions denoting sets of trees. The efficiency of their satisfiability test is a central issue in set-based program analysis, their main application domain. We introduce the class of set constraints with intersection (the only operators forming the expressions are constructors and intersection) and show that its satisfiability problem is DEXPTIME-complete. The complexity characterization continues to hold for negative set constraints with intersection (which have positive and negated inclusions). We reduce the satisfiability problem for these constraints to one over the interpretation domain of nonempty sets of trees. Set constraints with intersection over the domain of nonempty sets of trees enjoy the fundamental property of independence of negated conjuncts. This allows us to handle each negated inclusion separately by the entailment algorithm that we devise. We furthermore prove that set constraints with intersection are equivalent to the class of definite set constraints and thereby settle the complexity question of the historically first class for which the decidability question was solved.

BibTeX

  @InProceedings{CharatonikPodelski-Setconstraintswithi,
    author = 	 {Witold Charatonik and Andreas Podelski},
    title = 	 {Set constraints with intersection},
    booktitle =  {Proceedings of the Twelfth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1997},
    year =	 1997,
    editor =	 {Glynn Winskel},
    month =	 {June}, 
    pages =      {362--372},
    location =   {Warsaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }