# Item

ITEM ACTIONSEXPORT

Released

Report

#### Solving set constraints for greatest models

##### MPS-Authors

##### Locator

There are no locators available

##### Fulltext (public)

1997-2-004

(Any fulltext), 11KB

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

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

Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-9A35-B

##### Abstract

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.