A behavioral congruence for concurrent constraint programming with nondeterministic choice

Concurrent 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 (≈_sb), 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 ≈_sbis not a congruence for ccp with nondeterministic choice. We then introduce a new notion of bisimilarity, called weak full bisimilarity (≈f), and show that it is a congruence for the full language of ccp.We also show the adequacy of ≈f by establishing that it coincides with the congruence induced by closing ≈_sb under all contexts. The advantage of the new definition is that, unlike the congruence induced by ≈_sb, it does not require quantifying over infinitely many contexts.