Publication details

Saarland University Computer Science

Towards the verification of concurrent constraint programs in finite domain reasoning

Jörg Würtz

Post-conference workshop at ICLP: Verification and analysis of (concurrent) logic languages, pp. 87--107, June 1994

Combinatorial problems occur quite often in many application areas, e.g. scheduling or cutting stock problems, and may be specified as problems over finite domains, i.e., the variables range over a finite subset of the integers. Our approach taken in the concurrent constraint language Oz is to support an efficiently implementable constraint system for constraints 'x in D'. Using this constraint system, the programmer can add his own functionality by so called virtual constraints (e.g. 'x =< y'). Because the problem of satisfiability of these more complex constraints is NP-complete, most of them are implemented incompletely by using reflecting operators returning the current minimum and maximum of a variable's domain. For these programs serving as the core of finite domain reasoning, the question of verification arises. Verification is complicated by the operators reflecting the current known information about variables. In our approach we translate the computation states into first order formulas by giving virtual constraints their intended semantics (the semantics of the corresponding logic constraint). We prove that for a reduction of computation states Gamma -> Gamma' the corresponding first order formulas are equivalent with respect to the intended model. Our approach, which seems to be very natural in the setting of constraint languages, succeeds in proving virtual constraints to be correct, terminating and complete (in the shown example) with respect to an intended semantics.

Download PDF        Show BibTeX               

Login to edit

Legal notice, Privacy policy