A fully abstract model for concurrent constraint programming

Abstract

Recent results [5] have shown that concurrent Logic programming has a very simple model, based on linear sequences, which is fully abstract with respect to the parallel operator and finite observables. This is intrinsically related to the asynchronous and monotonic nature of the communication mechanism, which consists of asking and telling constraints on a common store. We consider here a paradigm for (asynchronous) concurrent programming, based on the above mechanism, and provided with the standard operators of choice, parallelism, prefixing, and hiding of local variables. It comes out that linear sequences still suffice for a compositional description of all the operators. Moreover, we consider the problem of full abstraction. Since our notion of observables implies the removal of silent steps, the presence of the choice operator induces the same problems (for compositionality) as bisimulation in CCS. We show that in our framework this problem has a simple solution which consists of introducing a semantical distinction between the various ways in which deadlock and failure might occur. The resulting semantics is fully abstract and still based on linear sequences.