A Behavioral Congruence for Concurrent Constraint Programming with Nondeterministic Choice

Abstract

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 ($\dot{\approx}_{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 $\dot{\approx}_{sb}$ is 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 $\dot{\approx}_{sb}$ under all contexts. The advantage of the new definition is that, unlike the congruence induced by $\dot{\approx}_{sb}$, it does not require quantifying over infinitely many contexts.

This work has been partially supported by the project ANR 12IS02001 PACE, ANR-09-BLAN-0169-01 PANDA, and by the French Defence procurement agency (DGA) with a PhD grant.