Solving set constraints for greatest models
Witold Charatonik, Andreas Podelski · 1997
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.