Bisimulation Techniques and Algorithms for Concurrent Constraint Programming

Andrés Aristizábal 1
1 COMETE - Concurrency, Mobility and Transactions
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : 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.
Document type :
Theses
Complete list of metadatas

Cited literature [62 references]  Display  Hide  Download

https://pastel.archives-ouvertes.fr/pastel-00756952
Contributor : Andres Alberto Aristizabal Pinzon <>
Submitted on : Saturday, November 24, 2012 - 2:34:21 PM
Last modification on : Wednesday, March 27, 2019 - 4:41:28 PM
Long-term archiving on : Monday, February 25, 2013 - 10:50:44 AM

Identifiers

  • HAL Id : pastel-00756952, version 1

Collections

Citation

Andrés Aristizábal. Bisimulation Techniques and Algorithms for Concurrent Constraint Programming. Other [cs.OH]. Ecole Polytechnique X, 2012. English. ⟨pastel-00756952⟩

Share

Metrics

Record views

719

Files downloads

1724