Concurrency is concerned with systems of multiple computing agents that interact with each other. Bisimilarity is one of the main representatives of these. Concurrent Constrain Programming (ccp) is a formalism that combines the traditional and algebraic view of process calculi with a declarative one based upon first-order logic. The standard definition of bisimilarity is not completely satisfactory for ccp since it yields an equivalence that is too fine grained. By building upon recent foundational investigations, we introduce a labeled transition semantics and a novel notion of bisimilarity that is fully abstract w.r.t. the observational equivalence in ccp. When the state space of a system is finite, the ordinary notion of bisimilarity can be computed via the partition refinement algorithm, but unfortunately, this algorithm does not work for ccp bisimilarity. Hence, we provide an algorithm that allows us to verify strong bisimilarity for ccp, modifying the algorithm by using a pre-refinement and a partition function based on the irredundant bisimilarity. Weak bisimilarity is a central behavioral equivalence in process calculi and it is obtained from the strong case by taking into account only the actions that are observable in the system. Typically the standard partition refinement can also be used for deciding weak bisimilarity simply by using Milner's reduction from weak to strong; a technique referred to as saturation. We demonstrate that the above-mentioned saturation technique does not work for ccp. We give a reduction that allows us to use the ccp partition refinement algorithm for deciding this equivalence.

Concurrence est concernée par les systèmes informatiques des agents multiples qui interagissent les uns avec les autres. Bisimilarité est l'un des principales représentantes de ces derniers. Programmation concurrente par contraintes (ccp) est un formalisme qui combine le point de vue traditionnel des formules algébriques et opérationnelles des calculs de processus avec une notion déclarative basée sur logique. La définition standard de bisimilarité n'est pas complètement satisfaisante pour ccp car il donne une équivalence qui est trop à grain fin. Nous introduisons une sémantique de transitions étiquetées et une notion de bisimilarité totalement abstraite à l'équivalence observationnelle en ccp. Lorsque l'espace d'état d'un système est fini, la notion ordinaire de bisimilarité peut être calculé par l'algorithme de partition de raffinement, mais, cet algorithme ne fonctionne pas pour la bisimilarité de ccp. Par conséquent, nous fournissons un algorithme que nous permet de vérifier bisimilarité forte pour ccp, en utilisant un pré-raffinement et une fonction de partition basée sur la bisimilarité irredondante. Bisimilarité faible est une équivalence comportementale obtenue en prenant en compte uniquement les actions qui sont observables dans le système. Typiquement, le raffinement de partition standard peut être utilisé pour décider bisimilarité faible simplement en utilisant la réduction de Milner allant de faible à forte. Nous démontrons que, en raison de ses impliquées transitions étiquetées, la technique mentionnée ci-dessus ne fonctionne pas pour ccp. Nous donnons une réduction qui nous permet d'utiliser cet algorithme pour ccp pour décider cette équivalence.