Efficient Verification and New Reasoning Techniques for Concurrent Constraint Programming (PhD Thesis)

Software, today more than ever, is part of our everyday life. From a smartphone to a tablet, to a laptop, these systems have changed the way we interact, think and work. More and more, we rely on a growing line of services that helps us to optimize our tasks. A good example is that of social networks; they basically consist of a set of individuals sharing and discussing about all kinds of ideas. These systems can be roughly described as (group of) agents that interact with each other by posting information in a shared-medium.

In this setting concurrent constraint programming language (CCP) [1] has much to offer. CCP is based on shared-memory communication where processes interact by adding and querying partial information represented as constraints (e.g., x > 42) in a global store. CCP is a mature linguistic formalism from the family of process calculi and hence it treats processes much like the λ-calculus treats computable functions. It provides a language in which the structure of terms represents the structure of processes together with an operational semantics to represent computational steps.

CCP 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 verification procedures for ccp have hitherto been far too little considered. This dissertation is focused on the development of novel reasoning techniques for program equivalence in ccp and their efficient verification.

The first part of the present thesis describes an algorithm for deciding strong bisimilarity (from [2]) for finite CCP processes. This is accomplished by first showing that the standard partition refinement approach [3, 4] does not work for CCP. Then, based on the work in [5], it is shown how to adapt the standard approach for the case of CCP. Furthermore, it is proven that this procedure suffers from the state explosion, common in the verification of concurrent systems, due mostly to the presence of non-deterministic choice.

The second part is devoted to the development of a weak semantics for CCP. As pointed out in the literature [6], one can use the procedure for strong bisimilarity to decide the weak one. The idea is to define a new transition relation based on the operational semantics, this method is known as saturation. The standard saturation is defined by omitting the silent transitions in the calculus. This works for CCS and other calculi, however in the case of CCP, because of its involved labeled transitions, it is shown that the standard technique is not complete for CCP. Then a new saturation is defined, we call it weak semantics for CCP. It consists in the reflexive and transitive closure under any constraint in CCP instead of just closing w.r.t. the silent transitions. Most importantly, it proven that the proposed weak semantics is sound and complete for CCP. As a consequence, the new saturation can be used for checking weak bisimilarity as in [6].

In the third part the focus is shifted towards efficiency on the verification of weak bisimilarity. To achieve this, a representative sub-language of CCP is considered: the summation-free fragment (CCP\+). First, it is shown that the verification algorithms described above have an exponential-time complexity even for programs from CCP\+. Then by exploiting confluence, a distinctive feature from this fragment, two alternative polynomial-time decision procedures for CCP\+ weak bisimilarity are proposed. Each of these two procedures has an advantage over the other. One has a better time complexity, while the other can be easily adapted for the full language of CCP to produce significant state space reductions. The relevance of both procedures derives from the importance of CCP\+. This fragment, which has been the subject of many theoretical studies, has strong ties to first-order logic and an elegant denotational semantics, and it can be used to model real-world situations. Most importantly, in [1] it was proven that weak bisimilarity in CCP\+ coincides with the standard observational equivalence for CCP\+ from [1]. Hence from the results presented in this part, two efficient algorithms for checking program equivalence in CCP\+ are obtained.

The last part addresses the congruence issue for the full language of CCP. It is shown that weak bisimilarity from [2] is not a congruence for CCP, as it is the case for weak bisimilarity in CCS. This problem is tackled by introducing a new notion that characterizes the weakest equivalence included in the congruence induced by weak bisimilarity for CCP. We call this new notion weak full bisimilarity. More importantly, it is proven that weak full bisimilarity is a congruence for the full language of CCP. It is also shown that weak full bisimilarity coincides with the standard notion of observational equivalence from [1] in CCP\+. To the best of our knowledge, this is the first notion of weak bisimilarity that is a congruence for the full language of CCP.