By Andrés Alberto Aristizábal Pinzón,
LIX – Ecole polytechnique
October 2012
Abstract
Concurrency is concerned with systems of multiple computing agents, usually called processes, that interact with each other. Bisimilarity is one of the main representative of these. It captures our intuitive notion of process equivalence. Concurrent Constraint Programming (ccp) is a well- established formalism that combines the traditional algebraic and operational view of process calculi with a declarative one based upon first-order logic.
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, we introduce a labelled transition semantics and a novel notion of bisimilarity that is fully abstract w.r.t. the typical observational equivalence in ccp.
When the state space of a system is finite, the ordinary notion of bisimilarity can be computed via the well-known 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 partition refinement algorithm by using a pre-refinement and a partition function based on the new notion of Irredundant bisimilarity.
Weak bisimiliarity is a central behavioural 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 bisimilarity; a technique referred to as saturation. We demonstrate that, because of its involved labeled transitions, the above- mentioned saturation technique does not work for ccp. We give an alternative reduction from weak ccp bisimilarity to the strong one that allows us to use the ccp partition refinement algorithm for deciding this equivalence.
Theoretical reasoning and manual verification based on correct mathematical and logical results make out a major branch in research in Computer Science. We can even say that this field is the cornerstone for developing and implementing reliable programs seldom prone to problems. Thus, we provide a complete and detailed description of a tool for verifying weak and strong bisimilarity for ccp in implementation terms.