MPI-INF/SWS Research Reports 1991-2017

2. Number - only D2


Solving set constraints for greatest models

Charatonik, Witold and Podelski, Andreas

November 1997, 12 pages.

Status: available - back from printing

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.

  • Attachement: ATTY9GKX (250 KBytes)

URL to this document:

Hide details for BibTeXBibTeX
  AUTHOR = {Charatonik, Witold and Podelski, Andreas},
  TITLE = {Solving set constraints for greatest models},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-97-2-004},
  MONTH = {November},
  YEAR = {1997},
  ISSN = {0946-011X},