×

Co-definite set constraints with membership expressions. (English) Zbl 0949.68017

Jaffar, Joxan (ed.), Logic programming. Proceedings of the joint international conference and symposium (JICSLP ’98), Manchester, GB, June 16-19, 1998. 4th joint event for the international conference on Logic programming (ICLP ’98) and the international logic programming symposium (ILPS ’98), and it is the 15th conference in each of the two series of premier international conference on Logic programming. Cambridge, MA: MIT Press. MIT Press Series in Logic Programming. 25-39 (1998).
Summary: Set constraints express inclusion and non-inclusion relationships between sets of trees using Boolean connectives, functional composition and “projections”. It is a suitable formalism for program-analysis (set-based analysis) and typing. Complexity of satisfiability of the general class is NEXPTIME-complete, and lots of works deal with subclasses, trying to get more tractable algorithms.
Recently, Podelski and Charatonik introduce the class of co-definite set constraints for analysis of reactive logic programs. They give an algorithm for deciding satisfiability – and “computing” the greatest solution – for this class interpreted over sets of infinite and finite trees. In this paper, we extend this result by adding membership expressions: they are more expressive and we show how they provide an easy abstraction mechanism of the \(T_P\) operator. We think that our method improves previous works also by its simplicity. We use the tree automaton framework both for computation and representation of the greatest solution. The algorithm we obtain is rather simple and concepts that we introduce for the proof seem to be interesting on their own rights.
For the entire collection see [Zbl 0930.00070].

MSC:

68N17 Logic programming

Keywords:

set constraints
PDFBibTeX XMLCite