de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Impressum Kontakt Einloggen
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Zeitschriftenartikel

Set Constraints with Intersection

MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44232

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

http://pubman.mpdl.mpg.de/cone/persons/resource/persons45201

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

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

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


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-000F-3070-7
Zusammenfassung
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.