Efficient Algorithms for Program Equivalence for Confluent Concurrent Constraint Programming

International audienceConcurrent Constraint Programming (CCP) is a well-established declarative frame-work from concurrency theory. Its foundations and principles e.g., semantics, proof systems, axiomatizations, have been thoroughly studied for over the last two decades. In contrast, the development of algorithms and automatic verifica-tion procedures for CCP have hitherto been far too little considered. To the best of our knowledge there is only one existing verification algorithm for the standard notion of CCP program (observational) equivalence. In this paper we first show that this verification algorithm has an exponential-time complexity even for pro-grams from a representative sub-language of CCP; the summation-free fragment (CCP\+). We then significantly improve on the complexity of this algorithm by providing two alternative polynomial-time decision procedures for CCP\+ pro-gram equivalence. Each of these two procedures has an advantage over the other. One has a better time complexity. The other can be easily adapted for the ful