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

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Bericht

Solving set constraints for greatest models

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)

1997-2-004
(beliebiger Volltext), 11KB

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

Charatonik, W., & Podelski, A.(1997). Solving set constraints for greatest models (MPI-I-1997-2-004). Saarbrücken: Max-Planck-Institut für Informatik.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-0014-9A35-B
Zusammenfassung
In set-based program analysis, one first infers a set constraint $\phi$ from a program and then, in a constraint-solving process, one transforms $\phi$ into an effective representation of sets of program values. Heintze and Jaffar have thus analyzed logic programs with respect to the least-model semantics. In this paper, we present a set-based analysis of logic programs with respect to the greatest model semantics, and we give its complexity characterization. We consider set constraints consisting of inclusions $x\subseteq\tau$ between a variable $x$ and a term $\tau$ with intersection, union and projection. We solve such a set constraint by computing a representation of its greatest solution (essentially as a tree automaton). We obtain that the problem of the emptiness of its greatest solution is DEXPTIME-complete. The choice of the greatest model for set-based analysis is motivated by the verification of safety properties (``no failure'') of reactive (ie, possibly non-terminating) logic programs over infinite trees. Therefore, we account also for infinite trees.