Project topics and materials
Get Complete Project Material File(s) Now! »
Concurrent Constraint Programming (CCP)
Concurrency theory studies the description and the analysis of systems consisting of interacting processes. Processes are typically viewed as infinite objects, in the sense that they can produce arbitrary and possibly endless interactions with their environment. Process calculi treat these processes much like the -calculus treats computable functions. They provide a formal language in which processes are represented by terms, and a set of rewriting rules to represent process evolution (or transitions). For example, the term P k Q represents the process that results from the parallel composition of the processes P and Q. A (labeled) transition P ! P 0 represents the evolution of P into P 0 given an interaction with the environment.
Concurrent Constraint Programming (CCP) [62, 63] is a mature formalism from concurrency theory that combines the traditional algebraic and operational view of process calculi with a declarative one based on first-order logic (see a survey in [47]). CCP processes can then be seen as computing agents as well as first-order logic formulae. In CCP, processes interact asynchronously by posting (or telling) and querying (or asking) information, traditionally referred to as con-straints, in a shared-medium referred to as the store. Furthermore, CCP is para-metric in a constraint system indicating interdependencies (entailment) between constraints and providing for the specification of data types and other rich struc-tures. The above features have recently attracted renewed attention as witnessed by the works [52, 19, 11, 10] on calculi exhibiting data-types, logic assertions as well as tell and ask operations. More recently in [36] the authors proposed the post and ask interaction model of CCP as an abstraction of social networks.
The features of CCP (and variants) have been used in a variety of applications in areas such as security, biology and multimedia interaction. For instance, CCP has been exploited to analyze security breaches in cryptographic protocols [48], for the prediction of organic malfunctions [31] and rhythmic coherence in music improvisation [59]. Furthermore, CCP foundations and principles e.g., semantics, proof systems, axiomatizations, have been thoroughly studied for over the last two decades. In contrast, as we previously argued the development of algorithms and automatic verification procedures for CCP have hitherto been far too little considered. In the next section we shall discuss the existing notions of equivalence for CCP.
Equivalences for CCP
In any computational model of processes, a central notion is that of behavioral equivalences [22]. In the case of CCP, the standard notion of observational equiv-alence from [63] ( o), roughly speaking, decrees that two CCP programs are observationally equivalent if each one can be replaced with the other in any CCP context and produce the same final result.
By process context, we mean a term C with a single hole such that if we replace with a process P , we obtain a process term C[P ]. For example, for the parallel context C = k R we obtain C[P ] = P k R:
Reasoning on processes and their equalities therefore means dealing with, and comparing, infinite structures. For this, a widely used mathematical tool is coinduction (see e.g. [4]). Coinduction is the dual of induction; while induction is a pervasive tool for reasoning about finite and stratified structures, coinduction of-fers similar strengths on structures that are circular or infinite. The most widely applied coinductive concept is bisimulation: bisimilarity is used to study behav-ioral equivalences, and the bisimulation proof method is used to prove such equiv-alences. In fact, most process calculi are equipped with a notion of bisimilarity.
Intuitively, for two processes, say P and Q, to be bisimilar one typically re-quires that whenever a process P performs an action and evolves to P 0, typically written P ! P 0, then Q must pick a successor Q0 such that Q ! Q0 where P 0 and Q0 are now bisimilar. The idea is then that two processes are strongly equivalent if they can mimic each other’s actions while arriving at equivalent suc-cessors. The intuition above corresponds, roughly speaking, to the standard notion of strong bisimilarity.
An alternative way of looking at bisimilarity is by using the so-called bisim-ulation game [53, 42] explained as follows. Given two players, called attacker and defender, the game starts with the attacker picking a transition P ! P 0 or Q ! Q0. Next the defender must reply by choosing a transition in Q ! Q0 or P ! P 0, respectively. Notice that they must perform the exact same ac-tion. Now if this game can be played forever then the defender wins, thus P and Q are considered strongly bisimilar. Otherwise, if the defender cannot reply successfully to the attacker, either because at the current process no transition is available, or no transition is tagged with the same action , then P and Q are not deemed strongly bisimilar.
There have been few attempts to define the notion of bisimilarity equivalence for CCP processes and they have not been completely satisfactory. The first one was proposed in the seminal work on the semantic foundations of CCP by Saraswat et al. [62]. Their bisimilarity is based on the standard bisimilarity we described above. Unfortunately, as shown in [6], the matching of actions from the game above was proven to be too fine grained; i.e. it may tell apart processes whose logical interpretation is identical.
Furthermore, similar notions were used in [68] to relate the fusion calculus with the -calculus, another concurrent constraint formalism. However, such no-tions are not defined for the -calculus itself. More recently, in [32] the author defines studies several notions of equivalence for linear CCP.
The latest attempt comes from [6] where the authors try to solve the aforemen-tioned problems by introducing a notion of bisimilarity for CCP called saturated barbed bisimilarity. The results obtained in [6] were part of the author’s master thesis, and for this reason they will be presented in the background material of the dissertation.
This approach is inspired by the notion of saturated bisimilarity from [14, 12] (pioneered by [46]). Intuitively, in order for two processes to be saturated bisimilar, (i) they should expose the same barbs, which are basic observations on the processes, (ii) whenever one of them moves then the other should reply and arrive at an equivalent process (i.e. follow a bisimulation game similar to the one described above), (iii) they should be equivalent under all the possible contexts of the language.
Nevertheless, to the best of our knowledge, none of these notions are provided with a decision procedure for their verification. Hence, one of the goals of this dissertation is to study whether the existing equivalences are adequate for CCP and to find efficient mechanisms to compute them, with particular emphasis on weak bisimilarity since it characterizes the standard notion of observational equivalence for CCP.
This Dissertation
We shall give some specific motivation and goals as well as a description of the approach we followed to obtain the results of this dissertation. Each of the sections below corresponds to a chapter in the present document.
Checking Strong Bisimilarity in CCP
Several efficient decision procedures and techniques for verifying bisimilarity have been developed [67, 25, 27]. But perhaps the best known is the partition refinement algorithm [34, 50]. This algorithm can be briefly explained as follows: First it generates the state space of a labeled transition system (LTS), i.e., the set of states reachable through the transitions. Then it creates a partition equating all states and finally, iteratively, it refines these partitions by splitting non equivalent states. The criteria for splitting partitions usually depends on the notion of bisim-ilarity, for instance, for the case of standard bisimilarity, the criteria would be the matching of actions (as described in the previous section). The resulting partition equates all and only bisimilar states.
In Chapter 3.1.2 we propose an adaptation of the partition refinement algo-rithm to decide strong saturated barbed bisimilarity ( sb) in CCP. Inspired by [3], the adaptation is based on the observation that some of the transitions are redundant, in the sense that they are logical consequences of other transitions. Unfortunately, such a notion of redundancy is not syntactic, but semantic, more precisely, it is based on sb itself.
A possible solution would be then to consider the transition system having only non-redundant transitions, thus the ordinary notion of bisimilarity coincides with sb. Hence, in principle, we could remove all the redundant transitions and then check bisimilarity with a standard algorithm. But how can we decide which transitions are redundant, if redundancy itself depends on sb ?
As we shall explain later on, the main idea is to compute sb and redun-dancy at the same time. In the first step, the algorithm deems all the states to be equivalent and all the (potentially redundant) transitions to be redundant. In any iteration, states are distinguished according to (the current estimation of) non-redundant transitions and then non-redundant transitions are updated according to the new computed partition.
One peculiarity of the algorithm in Chapter 3.1.2 is that in the initial parti-tion, we insert not only the reachable states, but also extra ones which are needed to check for redundancy. We shall see that, unfortunately, the number of these states might be exponentially bigger than the size of the original set of reachable states and therefore the worst-case complexity is exponential. To the best of our knowledge, this is the first algorithm for checking strong bisimilarity in CCP.
Reducing Weak to Strong Bisimilarity
In strong equivalences, and specifically strong bisimilarity, all the transitions per-formed by a system are deemed observable. In other words, we have seen how two processes are strongly bisimilar if and only if they can mimic each other’s actions, one by one. Instead in weak equivalences internal transitions are unobservable, namely transitions P ! P 0 which requires no interaction with the environment are invisible for this notion of equivalence. Internal transitions (also called re-ductions) are usually denoted by P ! P 0 where is an invisible action. On the one hand, weak equivalences are more abstract (and thus closer to the intu-itive notion of behavior); on the other hand, strong equivalences are usually much easier to check (for instance, in [37] a strong equivalence is introduced which is computable for a Turing complete formalism).
The weak version of sb is called weak saturated barbed bisimilarity ( sb) and it is defined as sb but in this case both the observations on processes (barbs) and the game may use zero or more steps (reductions) instead of exactly one. Following [2], the problem of checking weak bisimilarity can be reduced to the strong one. The standard reduction goes as follows. Given a (strong) LTS ! labeled with actions a; b; ; : : : one can build a (weak) LTS =) using the following inference rules:
P ! Q P =)P1 =) Q1 =) Q
P =)Q P =)P P =)Q
One can prove that weak bisimilarity on!a coincides with strong bisimilarity a on =). Hence weak bisimilarity can be checked with the algorithms for strong a bisimilarity on the new LTS =).
Unfortunately, in the case of CCP, the above assertion does not hold. In Chap-ter 4, we shall show that the standard method for reducing weak to strong bisim-ilarity does not work for CCP. The core of the problem lies on the actions per-formed by a CCP agent. Since the labels in the labeled transition system of a CCP agent are constraints, in fact, they are “the minimal constraints” that the store should satisfy in order to make the agent progress. These constraints form a lattice where the least upper bound (denoted by t) intuitively corresponds to con-junction and the bottom element is the constraint true. (As expected, transitions labeled by true are internal transitions, corresponding to the moves in standard process calculi).
As we shall explain in Chapter 4, in CCP, rather than closing the transitions just with respect to true, we shall need to close them with respect to all the con-straints. Formally we build the new LTS with the following rules.
P ! Q P =)Q=)R
a true atb
P =)Q P =)P P =)R
Notice that the above construction can also be done for CCS [41] by taking sequences of actions a; b rather than a t b. Nevertheless, the resulting transition system may be infinite-branching and hence not amenable to automatic verifica-tion using standard algorithms such as partition refinement.
Since in CCP we have that t is idempotent then if the original LTS !a has a finitely many transitions, then also =) is finite. This allows us to use the algo-rithm in Chapter 4 to check sb on (the finite fragment) of CCP. To the best of our knowledge, this is the first algorithm for checking weak bisimilarity in CCP.
Computing Bisimilarity in choice-free CCP
Despite being able to successfully compute bisimilarity in CCP, the methods in Chapters 3 and 4 briefly discussed previously are inefficient since they have an exponential time (and space) complexity.
The main goal of Chapter 5 is to produce efficient decision procedures for program equivalence for CCP. To achieve this, our approach is to restrict CCP to a meaningful fragment. Namely, the choice-free fragment of CCP, henceforth CCPn+. The CCPn+ formalism is perhaps the most representative sublanguage of CCP. It has been the subject of much theoretical study because of its computational expressivity, strong ties to first-order logic, and elegant denotational semantics based on closure operators [63]. Its most distinctive property is that of confluence in the sense that the final resulting store is the same regardless of the execution order of the parallel processes. We shall use this property extensively in proving the correctness of our decision procedures. Furthermore, from [6], we know that in this fragment sb coincides with the standard CCP observational equivalence for CCPn+ programs from [63].
When considering the weak equivalence sb and the approach from Chapter 4, confluence makes it possible to characterize redundant transitions syntactically, i.e., without any information about sb. Therefore for checking sb in CCPn+, we can first prune redundant transitions and then check the standard bisimilarity with one of the usual algorithms [34, 26, 16, 23]. Since redundancy can be determined statically, the additional states needed by the algorithm in Chapter 4 will not be necessary any more: in this way, the worst case complexity from exponential becomes polynomial. Unfortunately, this approach still suffers from the explosion of transitions caused by the “closure” of the transition relation. In order to avoid this prob-lem, we exploit a completely different approach (based on the semantic notion of compact input-output sets) that works directly on the original LTS. Intuitively, this approach consists of reducing the problem of checking sb in CCPn+ to the problem of whether the inputs have the same minimal finite representation regarding the outputs they produce in every possible context. We shall also show that the results obtained for CCPn+ can be exploited to optimize the partition refinement for the full language of CCP.
A Behavioral Congruence for CCP
The equivalences mentioned above determine what processes are deemed indis-tinguishable and they are expected to be congruences. The congruence issue is of great importance for algebraic and compositional reasoning: If two processes are equivalent, one should be able to replace one with the other in any context and preserve the equivalence (see e.g, [28]). For example, if ./ is a behavioral congruence, then P ./ Q should imply P k R ./ Q k R:
We shall build on a result of [6] showing that sb can be characterized by a novel bisimulation game (called, for simplicity, weak bisimulation) which relies at the same time on both barbs and labeled transitions. Recall that barbs are ba-sically predicates on the states, processes or configuration stating the observation we can make of them. This is rather peculiar with respect to the existing notions of bisimulation introduced for other process calculi where one usually exploits labeled transitions to avoid thinking about barbs and contexts. Indeed, labeled transitions usually capture barbs, in the sense that a state exposes a certain barb if and only if it performs a transition with a certain label. This is not the case in CCP, where barbs are observations on the store, while labeled transitions are determined by the processes. A more abstract understanding of this peculiarity of CCP can be given within the framework of [13] which is an extension of [38] featuring barbs and weak semantics.
As is customary for weak barbed equivalences, in our weak bisimulation game whenever a player exposes a barb #e, the opponent should expose the weak barb +e, i.e. it should be able to reach a state satisfying #e, but then the game restarts from the original state ignoring the arriving state. One of our contributions is to show that for CCP the arriving state cannot be ignored.
In Chapter 6 we shall show that the weak saturated barbed bisimilarity ( sb) [6] is not a congruence for CCP with nondeterministic choice. This problem is not particular to CCP, since many notions of weak bisimilarity are known not to be congruences in the presence of nondeterminism, for instance in CCS [42]. The problem is then to find a “good” variation of weak bisimilarity that is not too restrictive. For CCP, we introduce a new notion called weak full bisimilarity ( f ) and we prove that it is adequate for CCP since (i) it is a congruence for the full CCP and (ii) it corresponds to the weakest equivalence included in the congruence induced by sb. In fact, it is also adequate since in the choice-free fragment f corresponds to the standard notion of observational equivalence [63]. This is the first notion of weak bisimilarity that is a congruence for the full language of CCP.
Contributions and Organization
In this section we discuss the main contributions of this dissertation. Additionally, each chapter starts with an overview of its contents and ends with a detailed recap including a discussion of the related work.
Chapter 3. In this chapter we propose a decision procedure for verifying strong saturated barbed bisimilarity ( sb) in the finite fragment of CCP. To solve this problem we adapt the well-known partition refinement algorithm to the case of CCP, inspired by the results from [15]. We also explain in detail how to tackle the issues arising from the adaptation to CCP as well as the correctness and complex-ity of the algorithm proposed in this chapter. To the best of our knowledge, this is the first algorithm for the automatic verification of strong bisimilarity in CCP.
Chapter 4. In this chapter we introduce a weak semantics for CCP which can be used, together with the algorithm from Chapter 3, to verify weak saturated barbed bisimilarity ( sb) in the finite fragment of CCP. Intuitively, one can start from the labeled transition system generated using the operational semantics and then add some extra transitions, called weak transitions. Thus checking strong bisimilarity in the transformed input (with the new transitions) is equivalent to deciding weak bisimilarity in the original input. We prove that the standard way of defining the weak transitions, namely omitting the silent transitions, does not work for CCP. Similarly, we define a new weak semantics and we prove it adequate for CCP. Finally, using this new method, and based on Chapter 3, we propose a decision procedure to check sb. We conclude by proving the correctness and complexity of the algorithm defined in this chapter. To the best of our knowledge, this is the first algorithm for the automatic verification of weak bisimilarity in CCP.
Chapter 5. In this chapter we propose novel efficient methods for checking sb in a fragment of CCP. We first show that the algorithms from the previous chap-ters have an exponential time complexity even in the restricted case of finite CCP programs without nondeterministic choice. The main contribution of this chapter is the introduction of two novel decision procedures that can be used to decide sb for the finite choice-free fragment of CCP in polynomial time. This is achieved by exploiting certain distinctive features of this fragment such as confluence. Each of these two new procedures has an advantage over the other. One has a better time complexity. The other can be easily adapted for the full language of CCP to produce significant state space reductions. Recall that from [6] we know that, in the absence of nondeterminism, sb coincides with the standard notion of observational equivalence ( o) for CCP from [63], hence from this chapter we obtain two polynomial decision procedures to decide program equivalence in choice-free CCP.
Chapter 6. In this chapter, we tackle the congruence issues related to sb. First we prove that sb is a congruence for CCP without nondeterministic choice but not for the full language of CCP. We then propose a new notion of bisimilarity, called weak full bisimilarity ( f ). We show that f is a congruence for the full language of CCP. We also show the adequacy of the new notion by establishing that it is the largest congruence included in sb. In other words f coincides with the congruence induced by closing sb under all contexts. Beyond being a con-gruence, the advantage of f is that it does not require quantifying over infinitely many contexts. This is also important as it may simplify decision procedures for the equivalence. To the best of our knowledge, this is the first behavioral equiv-alence, which does not appeal to quantification over arbitrary process contexts in its definition, that is a congruence for CCP with nondeterministic choice.
Remark 1.4.1. Part of the material in Chapters 3 and 4 is also included in the thesis of Aristizabal [5]. However, those chapters are based on the journal paper [54] instead of [8, 7] as in [5].
Chapters 3 and 4 are a generalization of the results in [8, 7]. This version includes more detailed explanations and essential corrections to the original ma-terial. It also contains new contributions such as the specification of the algorithm for deciding observational equivalence in CCP.
Publications from this Dissertation
The material in the present thesis has been published in the following papers:
Journals in the Journal of Science of Computer Programming, 2015.
DOI: http://dx.doi.org/10.1016/j.scico.2014.12.003.
The contributions of this paper are presented in Chapter 5 and 6.
Proceedings of International Conferences
[8] A. Aristizabal, F. Bonchi, L. Pino, F. Valencia, Partition Refinement for Bisimilarity in CCP, in: S. Ossowski, P. Lecca (Eds.), Proceedings of the 27th Annual ACM Symposium on Applied Computing (SAC 2012), Constraint Solving and Programming Track, ACM, 2012, pp. 88-93.
DOI: http://dx.doi.org/10.1145/2245276.2245296. The contributions of this paper are presented in Chapter 3.
[56] L. Pino, F. Bonchi, F. Valencia, Efficient Computation of Program Equivalence for Confluent Concurrent Constraint Programming, in: R. Pena,˜ T. Schrijvers (Eds.), Proceedings of the 15th International Symposium on Principles and Practice of Declarative Programming (PPDP 2013), ACM, 2013, pp. 263-274.
DOI: http://dx.doi.org/10.1145/2505879.2505902.
The contributions of this paper are presented in Chapter 5.
[58] L. Pino, F. Bonchi, F. Valencia. A Behavioral Congruence for Con-current Constraint Programming with Non-deterministic Choice, in: In G. Ciobanu and D. Mery´ (Eds.), Proceedings of the 11th International Collo-quium on Theoretical Aspects of Computing (ICTAC 2014), volume 8687 of Lecture Notes in Computer Science, pages 351-368. Springer, 2014.
DOI: http://dx.doi.org/10.1007/978-3-319-10882-7_21 The contributions of this paper are presented in Chapter 6.
Proceedings of International Workshops
[7] A. Aristizabal, F. Bonchi, L. Pino, F. Valencia, Reducing Weak to Strong Bisimilarity in CCP, in: M. Carbone, I. Lanese, A. Silva, A. Sokolova (Eds.), Proceedings of the 5th Interaction and Concurrency Experience (ICE 2012), volume 104 of Electronic Proceedings in Theoretical Computer Sci-ence, 2012, pp. 2-16.
DOI: http://dx.doi.org/10.4204/EPTCS.104.2.
The contributions of this paper are presented in Chapter 4.
Extended abstract with informal proceedings [57] L. Pino, F. Bonchi, F. Valencia. Efficient Computation of Program Equivalence for Confluent Concurrent Constraint Programming (Extended Abstract). (Informal) Proceedings of the 5th Young Researchers Workshop on Concurrency Theory (YR-CONCUR 2013).
Table of contents :
1 Introduction
1.1 Motivation
1.2 Context
1.2.1 Concurrent Constraint Programming (CCP)
1.2.2 Equivalences for CCP
1.3 This Dissertation
1.3.1 Checking Strong Bisimilarity in CCP
1.3.2 Reducing Weak to Strong Bisimilarity
1.3.3 Computing Bisimilarity in choice-free CCP
1.3.4 A Behavioral Congruence for CCP
1.4 Contributions and Organization
1.5 Publications from this Dissertation
2 Preliminaries
2.1 Domain theory
2.2 Labeled Transition System, Partition and Graphs
2.3 Partition Refinement
2.4 Concurrent Constraint Programming (CCP)
2.4.1 Constraint Systems
2.4.2 Syntax of CCP
2.4.3 Reduction Semantics
2.4.4 Barbed Semantics and Barbed Bisimilarity
2.4.5 Observational Equivalence
2.4.6 Labeled Semantics
2.4.7 Soundness and Completeness
2.4.8 Strong and Weak Labeled Bisimilarity
3 Verifying Strong Bisimilarity in CCP
3.1 Partition Refinement for CCP
3.1.1 Derivation and Domination
3.1.2 The Algorithm
3.2 Correctness and Complexity
3.2.1 Irredundant and Symbolic Bisimilarity
3.2.2 Proof of Correctness and Complexity
3.3 Summary and Related Work
4 A Weak Semantics for CCP
4.1 The standard reduction from weak to strong
4.1.1 Incompleteness of Milner’s saturation method in CCP
4.2 Reducing Weak Bisimilarity to Strong in CCP
4.2.1 Defining a new saturation method for CCP
4.2.2 The new saturation method is finitely branching
4.2.3 A Remark about our Saturation in CCS
4.2.4 Soundness and Completeness
4.3 Deciding Weak Bisimilarity
4.3.1 Weak Irredundant andWeak Saturated Bisimilarity coincide
4.3.2 Algorithm for weak bisimilarity in CCP
4.4 Summary and Related Work
5 Computing bisimilarity in Choice-Free CCP
5.1 Using Partition Refinement in choice-free CCP
5.1.1 Properties of CCP without choice
5.1.2 Optimizing partition refinement for choice-free CCP
5.2 The compact input-output sets approach
5.2.1 Weak bisimilarity and barb equivalence
5.2.2 A canonical representation of choice-free configurations
5.3 Improving the general partition refinement for CCP
5.4 Summary and Related Work
6 A Behavioral Congruence for CCP
6.1 Congruence issues
6.2 Weak full bisimilarity
6.2.1 More than weak barbs
6.2.2 Full Bisimilarity is a Congruence
6.2.3 Relation with observational equivalence
6.2.4 Behavioral congruence
6.3 Summary and Related Work
7 Conclusions
7.1 Summary
7.2 Future Work
