Concurrent Constraint Programming (CCP) is a well-established model for concurrency that builds upon operational and algebraic notions from process calculi and first-order logic. Bisimilarity is one of the central reasoning techniques in concurrency. The standard definition of bisimilarity, however, is not completely satisfactory for CCP since it yields an equivalence that is too fine grained. By building upon recent foundational investigations (stemmed from the theory of Reactive Systems), we introduce a labelled transition semantics and a novel notion of bisimilarity that is fully abstract with respect to the typical observational equivalence in CCP. This way we provide CCP with a new proof technique that is coherent with existing ones.

Joint work with Andres Aristizabal, Catuscia Palamidessi, Luis Pino, Frank Valencia.