Item

Abstract

Testing satisfaction of guards is the essential operation of concurrent constraint programming ({\footnotesize CCP}) systems. We present and prove correct, for the first time, an incremental algorithm for the simultaneous tests of entailment and disentailment of rational tree constraints to be used in {\footnotesize CCP} systems with deep guards (\eg, in {\footnotesize AKL} or in Oz). The algorithm is presented as the {\em simplification\/} of the constraints which form the (possibly deep) guards and which are {\em situated\/} at different nodes in a tree (of arbitrary depth). The nodes correspond to local computation spaces. In this algorithm, a variable may have multiple bindings (which each represent a constraint on that same variable in a different node). These may be realized in various ways. We give a simple fixed-point algorithm and use it for proving that the tests implemented by another, practical algorithm are correct and complete for entailment and disentailment. We formulate the results in this paper for rational tree constraints; they can be adapted to finite and feature trees.