A Behavioral Congruence for Concurrent Constraint Programming with Non-deterministic Choice

International audienceConcurrent constraint programming (CCP) is a well-established model of concurrency for reasoning about systems of multiple agents that interact with each other by posting and querying partial information on a shared space. (Weak) bisimilarity is one of the most representative notions of behavioral equivalence for models of concurrency. A notion of weak bisimilarity, called weak saturated bisimilarity (WSB), was recently proposed for CCP. This equivalence improves on previous bisimilarity notions for CCP that were too discriminating and it is a congruence for the choice-free fragment of CCP. In this paper, however, we show that WSB is not a congruence for CCP with nondeterministic choice. We then introduce a new notion of bisimilarity, called weak full bisimilarity (FB), and show that it is a congruence for the full language of ccp. We also show the adequacy of FB by establishing that it coincides with the congruence induced by closing WSB under all contexts. The advantage of the new definition is that, unlike the congruence induced by WSB, it does not require quantifying over infinitely many contexts