首页 | 本学科首页   官方微博 | 高级检索  
     


Set Constraints with Intersection
Authors:Witold Charatonik  Andreas Podelski
Affiliation:a Max-Planck-Institut für Informatik Im Stadtwald, Saarbrücken, D-66123, Germanyf1;b University of Wroclaw, Poland;c Max-Planck-Institut für Informatik Im Stadtwald, Saarbrücken, D-66123, Germanyf2
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.
Keywords:
本文献已被 ScienceDirect 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号