Luis F Pino
email: luis.pino@lix.polytechnique.fr

Andres Aristizabal
email: aaaristizabal@javerianacali.edu.co

Filippo Bonchi
email: filippo.bonchi@ens-lyon.fr

Frank Valencia
email: frank.valencia@lix.polytechnique.fr

Andrés Aristizábal

Weak CCP bisimilarity with strong procedures

Keywords: Concurrent Constraint Programming, Weak bisimilarity, Partition refinement

Concurrent constraint programming (CCP) is a well-established model for concurrency that singles out the fundamental aspects of asynchronous systems whose agents (or processes) evolve by posting and querying (partial) information in a global medium. Bisimilarity is a standard behavioral equivalence in concurrency theory. However, only recently a well-behaved notion of bisimilarity for CCP, and a CCP partition refinement algorithm for deciding the strong version of this equivalence have been proposed. 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 us-

Introduction

Since the introduction of process calculi, one of the richest sources of foundational investigations stemmed from the analysis of behavioral equivalences: in any formal process language, systems which are syntactically different may denote the same process, i.e., they have the same observable behavior.

A major dichotomy among behavioral equivalences concerns strong and weak equivalences. In strong equivalences, all the transitions performed by a system are deemed observable. In weak equivalences, instead, internal transitions (usually denoted by τ ) are unobservable. On the one hand, weak equivalences are more abstract (and thus closer to the intuitive notion of behavior); on the other hand, strong equivalences are usually much easier to be checked (for instance, in [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF] a strong equivalence is introduced which is computable for a Turing complete formalism).

Strong bisimilarity is one of the most studied behavioral equivalence and many algorithms (e.g., [START_REF] Victor | The mobility workbench -a tool for the π-calculus[END_REF][START_REF] Fernandez | An implementation of an efficient algorithm for bisimulation equivalence[END_REF][START_REF] Ferrari | Verifying mobile processes in the HAL environment[END_REF]) have been developed to check whether two systems are equivalent up to strong bisimilarity. Among these, the partition refinement algorithm [START_REF] Kanellakis | CCS expressions, finite state processes, and three problems of equivalence[END_REF][START_REF] Paige | Three partition refinement algorithms[END_REF] is one of the best known: 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 afterwards, iteratively, refines these partitions by splitting non equivalent states. At the end, the resulting partition equates all and only bisimilar states.

Weak bisimilarity can be computed by reducing it to strong bisimilarity. Given a (strong) LTS -→ labeled with actions a, b, τ, . . . one can build a (weak) LTS =⇒ using the following inference rules:

P a -→ Q P a =⇒ Q P τ =⇒ P P τ =⇒ P 1 a =⇒ Q 1 τ =⇒ Q P a =⇒ Q
Since weak bisimilarity on a -→ coincides with strong bisimilarity on a =⇒, then one can check weak bisimilarity with the algorithms for strong bisimilarity on the new LTS a =⇒. Concurrent Constraint Programming (CCP) [START_REF] Saraswat | Concurrent constraint programming[END_REF] is a formalism that combines the traditional algebraic and operational view of process calculi with a declarative one based on first-order logic. In CCP, processes (agents or programs) interact by adding (or telling) and asking information (namely, constraints) in a medium (the store). Inspired by [START_REF] Bonchi | Saturated semantics for reactive systems[END_REF][START_REF] Bonchi | Reactive systems, barbed semantics, and the mobile ambients[END_REF], the authors introduced in [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF] both strong and weak bisimilarity for CCP and showed that the weak equivalence is fully abstract with respect to the standard observational equivalence of [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF]. Moreover, a variant of the partition refinement algorithm is given in [START_REF] Aristizábal | Partition refinement for bisimilarity in CCP[END_REF] for checking strong bisimilarity on (the finite fragment of) concurrent constraint programming.

In this paper, first we show that the standard method for reducing weak to strong bisimilarity does not work for CCP and then we provide a way out of the impasse. Our solution can be readily explained by observing that the labels in the LTS of a CCP agent are constraints (actually, 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 ⊔) intuitively corresponds to conjunction 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). Now, rather than closing the transitions just with respect to true, we need to close them w.r.t. all the constraints. Formally we build the new LTS with the following rules.

P a -→ Q P a =⇒ Q P true =⇒ P P a =⇒ Q b =⇒ R P a⊔b =⇒ R
The above construction can also be done for CCS [START_REF] Milner | A Calculus of Communicating Systems[END_REF] by taking sequences of actions a; b rather than a ⊔ b. Nevertheless, the resulting transition system may be infinite-branching and hence not amenable to automatic verification using standard algorithms such as partition refinement. In the case of CCP instead, since ⊔ is idempotent, if the original LTS a -→ has finitely many transitions, then also a =⇒ is finite. This allows us to use the algorithm in [START_REF] Aristizábal | Partition refinement for bisimilarity in CCP[END_REF] to check weak bisimilarity on (the finite fragment) of concurrent constraint programming.

We have developed a tool in which this procedure is implemented. To the best of our knowledge, it is the first tool for checking weak bisimilarity for CCP. It can be found at: http://www.lix.polytechnique.fr/ ˜andresaristi/ checkers/ Contributions. This paper is an extended version of [START_REF] Aristizábal | Reducing weak to strong bisimilarity in CCP[END_REF]. In this version we give all the details and proofs omitted in [START_REF] Aristizábal | Reducing weak to strong bisimilarity in CCP[END_REF]. We generalize some notions, add new examples and extend the intuitions from [START_REF] Aristizábal | Reducing weak to strong bisimilarity in CCP[END_REF] to improve the clarity of the paper. Furthermore, in Section 3.1.3 we illustrate why our technique would not work for CCS-like process calculi in which two labels cannot be joined into a single one like in CCP. We also add a new section, Section 4, that includes the specification of the algorithm for observational equivalence in CCP, as well as its proof of correctness and complexity. This new section also includes some experiments comparing the strong and weak bisimilarity procedures.

Related Work. CCP is not the only formalism where weak bisimilarity cannot be naively reduced to the strong one. Probably the first case in literature can be found in [START_REF] Victor | The mobility workbench -a tool for the π-calculus[END_REF] that introduces an algorithm for checking weak open bisimilarity of π-calculus. This algorithm is rather different from ours, since it is on-the-fly [START_REF] Fernandez | An implementation of an efficient algorithm for bisimulation equivalence[END_REF] and thus it checks the equivalence of only two given states (while our algorithm, and more generally all algorithms based on partition refinement, check the equivalence of all the states of a given LTS). These algorithms have a polynomial upper bound time complexity. The present algorithm has an exponential time complexity. However, they deal with very different formalisms. Also [START_REF] Baldan | A semantic framework for open processes[END_REF] defines weak labeled transitions following the above-mentioned standard method which does not work in the CCP case.

Analogous problems to the one discussed in this paper arise in Petri nets [START_REF] Sobocinski | Representations of petri net interactions[END_REF][START_REF] Bruni | A connector algebra for p/t nets interactions[END_REF], in tile transition systems [START_REF] Gadducci | The tile model[END_REF][START_REF] Bruni | Deriving weak bisimulation congruences from reduction systems[END_REF] and, more generally, in the theory of reactive systems [START_REF] Sewell | From rewrite rules to bisimulation congruences[END_REF][START_REF] Leifer | Transition systems, link graphs and petri nets[END_REF][START_REF] Jensen | Mobile Processes in Bigraphs[END_REF] (the interested reader is referred to [START_REF] Sobocinski | Relational presheaves as labelled transition systems[END_REF] for an overview). In all these cases, labels form a monoid where the neutral element is the label of internal transitions. In the case of CCS, the fact that a system may perform a transition with a composed label a; b means that it may perform first a transition with a and then a transition with b. This property, which in tile systems [START_REF] Gadducci | The tile model[END_REF][START_REF] Bruni | Deriving weak bisimulation congruences from reduction systems[END_REF] is known as vertical decomposition, does not hold for CCP and for the other formalisms mentioned above. As a consequence of this fact, when reducing from weak to strong bisimilarity, one needs to close the transitions with respect to the composition of the monoid (and not only with respect to the neutral element). However, usually, labels composition is not idempotent (as it is for CCP) and thus a finite LTS might be transformed into an infinite one. For this reason, this procedure applied to the afore mentioned cases is not effective for automatic verification.

The result presented in this paper, and more generally our research on CCP, has been largely inspired by the theory of reactive systems by Leifer and Milner [24]: in our operational semantics of CCP, labels represent the "minimal" constraints that the store should satisfy for executing some transitions, while in [START_REF] Leifer | Deriving bisimulation congruences for reactive systems[END_REF], labels are the "minimal" contexts.

Structure of the paper. In Section 2 we recall the partition refinement method and the standard reduction from weak to strong bisimilarity. We also recall the CCP formalism, its equivalences, and the CCP partition refinement algorithm. We then show why the standard reduction does not work for CCP. In Section 3 we present our reduction and show its correctness. Finally in Section 4 discuss the decision procedure for observational equivalence in CCP.

From Weak to Strong Bisimilarity: Saturation Approach

We start this section by recalling the notion of labeled transition system (LTS), partition and the graph induced by an LTS. Then we present the standard partition refinement algorithm for checking strong bisimilarity, and also how to use it to verify weak bisimilarity. Next we introduce concurrent constraint programming (CCP) including the partition refinement algorithm for CCP. Finally, we shall show that the standard reduction from weak to strong bisimilarity does not work for CCP. Labeled Transition System. A labeled transition system (LTS) is a triple (S, L, ) where S is a set of states, L a set of labels and ⊆ S × L × S a transition relation. We shall use s a r to denote the transition (s, a, r) ∈ . Given a transition t = (s, a, r) we define the source, the target and the label as follows src(t) = s, tar (t) = r and lab(t) = a. We assume the reader to be familiar with the standard notion of bisimilarity [START_REF] Milner | A Calculus of Communicating Systems[END_REF].

Partition. Given a set S, a partition P of S is a set of non-empty blocks, i.e., subsets of S, that are all disjoint and whose union is S. We write {B 1 } . . . {B n } to denote a partition consisting of (non-empty) blocks B 1 , . . . , B n . A partition represents an equivalence relation where equivalent elements belong to the same block. We write sPr to mean that s and r are equivalent in the partition P.

LTSs and Graphs. Given a LTS (S, L, ), we write LTS for the directed graph whose vertices are the states in S and edges are the transitions in . Given a set of initial states IS ⊆ S, we write LTS (IS ) for the subgraph of LTS rechable from IS . Given a graph G we write V(G) and E(G) for the set of vertices and edges of G, respectively.

s s ′ s ′′ a a s, s ′ , s ′′ s, s ′ s ′′ s s ′ s ′′ P F (P) F (F (P))
Figure 1: An example of the use of F (P) from Equation 12

.1. Partition Refinement

We recall the partition refinement algorithm [START_REF] Kanellakis | CCS expressions, finite state processes, and three problems of equivalence[END_REF] for checking bisimilarity over the states of an LTS (S, L, ).

Given a set of initial states IS ⊆ S, the partition refinement algorithm (see Algorithm 1) checks bisimilarity on IS as follows. First, it computes IS ⋆ , that is the set of all states that are reachable from IS using . Then it creates the partition P 0 where all the elements of IS ⋆ belong to the same block (i.e., they are all equivalent). After the initialization, it iteratively refines the partitions by employing the function on partitions F (-), defined as follows: for a partition P, sF (P)r iff if s a s ′ then exists r ′ s.t. r a r ′ and s ′ Pr ′ .

(1)

See Figure 1 for an example of F (P). Algorithm 1 terminates whenever two consecutive partitions are equivalent. In such a partition two states (reachable from IS ) belong to the same block iff they are bisimilar (using the standard notion of bisimilarity [START_REF] Milner | A Calculus of Communicating Systems[END_REF]).

Algorithm 1 pr(IS , ) Initialization

1. IS ⋆ is the set of all states reachable from IS using , 2. P 0 := IS ⋆ , Iteration P n+1 := F (P n ) as in Equation 1Termination If P n = P n+1 then return P n . Standard reduction from weak to strong bisimilarity. As pointed out in the literature (Chapter 3 in [START_REF] Sangiorgi | Advanced Topics in Bisimulation and Coinduction[END_REF]), in order to compute weak bisimilarity, we can use the above-mentioned partition refinement. The idea is to start from the LTS generated using the operational semantics (-→) and then saturate it using the rules described in Table 1. Now the problem whether two states s and s ′ are weakly bisimilar can be reduced to checking whether they are strongly bisimilar w.r.t. =⇒. Formally, we can call pr({s, s ′ }, =⇒) to check whether s and s ′ are weakly bisimilar. Henceforth, we shall refer to this as Milner's saturation method.

As we will show later on, this approach does not work in a formalism like CCP. We shall see that the problem is related to the fact that the transitions in CCP are labeled with constraints, thus they can be arbitrary combined (using the least upper bound operator) to form a new label. Notice that this is not the case for the transitions in CCS-like process calculi. Therefore we will need to define a different saturation method to be able to use the saturation approach for verifying weak bisimilarity in CCP. Namely, we will modify the rules in Table 1 so we can still use the standard strategy for deciding observational equivalence in CCP.

Concurrent Constraint Programming (CCP)

We shall now recall CCP and the adaptation of the partition refinement algorithm to compute bisimilarity in CCP [START_REF] Aristizábal | Partition refinement for bisimilarity in CCP[END_REF].

Constraint Systems

The CCP model is parametric in a constraint system (cs) specifying the structure and interdependencies of the information that processes can ask or and add to a central shared store. This information is represented as assertions traditionally referred to as constraints. Following [START_REF] De Boer | Nondeterminism and infinite computations in constraint programming[END_REF][START_REF] Mendler | A logical view of concurrent constraint programming[END_REF] we regard a cs as a complete algebraic lattice in which the ordering ⊑ is the reverse of an entailment relation: c ⊑ d means d entails c, i.e., d contains "more information" than c. The top element false represents inconsistency, the bottom element true is the empty constraint, and the least upper bound (lub) ⊔ is the join of information.

Definition 1 (cs). A constraint system (cs) C = (Con, Con 0 , ⊑, ⊔, true, false) is a complete algebraic lattice where Con, the set of constraints, is a partially ordered set wrt ⊑, Con 0 is the subset of compact elements of Con, ⊔ is the lub operation defined on all subsets, and true, false are the least and greatest elements of Con, respectively.

Recall that C is a complete lattice if every subset of Con has a least upper bound in Con. An element c ∈ Con is finite if for any directed subset D of Con, c ⊑ D implies c ⊑ d for some d ∈ D. C is algebraic if each element c ∈ Con is the least upper bound of the finite elements below c.

In order to model hiding of local variables and parameter passing, in [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF] the notion of constraint system is enriched with cylindrification operators and diagonal elements, concepts borrowed from the theory of cylindric algebras (see [START_REF] Monk | Cylindric Algebras (Part I)[END_REF]).

Let us consider a (denumerable) set of variables Var with typical elements x, y, z, . . . Define ∃ Var as the family of operators ∃ Var = {∃ x | x ∈ Var } (cylindric operators) and D Var as the set D Var = {d xy | x, y ∈ Var } (diagonal elements).

A cylindric constraint system over a set of variables Var is a constraint system whose underlying support set Con ⊇ D Var is closed under the cylindric operators ∃ Var and quotiented by Axioms C1 -C4, and whose ordering ⊑ satisfies Axioms C5 -C7 :

C1. ∃ x ∃ y c = ∃ y ∃ x c C2. d xx = true C3. if z = x, y then d xy = ∃ z (d xz ⊔ d zy ) C4. ∃ x (c ⊔ ∃ x d) = ∃ x c ⊔ ∃ x d C5. ∃ x c ⊑ c C6. if c ⊑ d then ∃ x c ⊑ ∃ x d C7. if x = y then c ⊑ d xy ⊔ ∃ x (c ⊔ d xy )
where c, c i , d indicate finite constraints, and ∃ x c ⊔ d stands for (∃ x c) ⊔ d. For our purposes, it is enough to think the operator ∃ x as existential quantifier and the constraint d xy as the equality x = y.

Cylindrification and diagonal elements allow us to model the variable renaming of a formula φ; in fact, by the aforementioned axioms, we have that the formula ∃ x (d xy ⊔ φ) = true can be depicted as the formula φ[y/x], i.e., the formula obtained from φ by replacing all free occurrences of x by y.

We assume notions of free variable and of substitution that satisfy the following conditions, where c[y/x] is the constraint obtained by substituting x by y in c and fv (c) is the set of free variables of c:

(1) if y / ∈ fv (c) then (c[y/x])[x/y] = c; (2) (c⊔d)[y/x] = c[y/x]⊔d[y/x]; (3) x / ∈ fv (c[y/x]); (4) fv (c⊔d) = fv (c)∪fv (d).
Example 1 (A Constraint System of Linear Order Arithmetic). Consider the following syntax: φ, ψ . . .

:= t = t ′ | t > t ′ | φ ∨ ψ | ¬φ
where the terms t, t ′ can be elements of a set of variables Var , or constant symbols 0, 1, . . .. Assume an underlying first-order structure of linear-order arithmetic with the obvious interpretation in the natural numbers ω of =, > and the constant symbols.

A variable assignment is a function µ : Var -→ ω. We use A to denote the set of all assignments; P(X) to denote the powerset of a set X, ∅ the empty set and ∩ the intersection of sets. We use M(φ) to denote the set of all assignments that satisfy the formula φ, where the definition of satisfaction is as expected.

We can now introduce a constraint system as follows: the set of constraints is P(A), and define c ⊑ d iff c ⊇ d. The constraint false is ∅, while true is A. Given two constraints c and d, c ⊔ d is the intersection c ∩ d. By abusing the notation, we will often use a formula φ to denote the corresponding constraint, i.e., the set of all assignments satisfying φ. E.g. we use x > 1 ⊑ x > 5 to mean M(x > 1) ⊑ M(x > 5). For this constraint system one can show that e is a compact constraint (i.e., e is in Con 0 ) iff e is a co-finite set in A (i.e., iff the complement of e in A is a finite set). For example, x > 10 ∧ y > 42 is a compact constraint for Var = {x, y}.

From this structure, let us now define the cylindric constraint system S as follows. We say that an assignment µ ′ is an x-variant of µ if ∀y = x, µ(y) = µ ′ (y). Given x ∈ Var and c ∈ P(A), the constraint ∃ x c is the set of assignments µ such that exists µ ′ ∈ c that is an x-variant of µ. The diagonal element d xy is x = y. Remark 1. We shall assume that the constraint system is well-founded and, for practical reasons, that its ordering ⊑ is decidable.

Processes

We now recall the basic CCP process constructions.

Syntax. Let us presuppose a constraint system C = (Con, Con 0 , ⊑, ⊔, true, false).

The CCP processes are given by the following syntax:

P, Q ::= stop | tell(c) | ask(c) → P | P Q | P + Q | ∃ x P
where c, e ∈ Con 0 and x ∈ Var . We use Proc to denote the set of all processes.

Finite processes. Intuitively, stop represents termination, the tell process tell(c) adds c to the global store. This addition is performed regardless of the generation of inconsistent information. The ask process ask(c) → P may execute P if c is entailed by the information in the store. The processes P Q and P + Q stand, respectively, for the parallel execution and non-deterministic choice of P and Q; ∃ x is a hiding operator, namely it indicates that in ∃ x P the variable x is local to P . The occurrences of x in ∃ x P are said to be bound. The bound variables of P , bv (P ), are those with a bound occurrence in P , and its free variables, fv (P ), are those with an unbound occurrence1 .

Remark 2. In this paper we restrict the CCP syntax to finite processes, since we shall deal with infinite-state transition system. Typically, to specify infinite behavior, CCP provides parametric process definitions. A process p( z) is said to be a procedure call with identifier p and actual parameters z. For each procedure call p(z 1 . . . z m ) there exists a unique (possibly recursive) procedure definition of the form p(x 1 . . . x m ) def = P where fv (P ) ⊆ {x 1 , . . . , x m }. Furthermore recursion is required to be guarded, i.e., each procedure call within P must occur within an ask process. The behavior of p(z 1 . . . z m ) is that of P [z 1 . . . z m /x 1 . . . x m ], i.e., P with each x i replaced with z i (applying α-conversion to avoid clashes).

Reduction Semantics

The operational semantics of CCP is given by an unlabeled transition relation between configurations. A configuration is a pair P, d representing a state of a system; d is a constraint representing the global store, and P is a process, i.e., a term of the syntax. We use Conf with typical elements γ, γ ′ , . . . to denote the set of configurations. A transition γ -→ γ ′ intuitively means that the configuration γ can reduce to γ ′ . We call these kind of unlabeled transitions reductions and we use -→ * to denote the reflexive and transitive closure of -→. Formally, the reduction semantics of CCP is given by the relation -→ defined in Table 2.

Rules R1, R3 and R4 are easily seen to realize the intuitions described in Section 2.2.2. Rule R2 states that ask(c) → P can evolve to P whenever the global store d entails c. Rule R5 is somewhat more involved. Intuitively, ∃ e

x P behaves like P , except that the variable x possibly present in P must be considered local, and that the information present in e has to be taken into account. 2 It is convenient to distinguish between the external and the internal points of view.

R1 tell(c), d -→ stop, d ⊔ c R2 c ⊑ d ask (c) → P, d -→ P, d R3 P, d -→ P ′ , d ′ P Q, d -→ P ′ Q, d ′ R4 P, d -→ P ′ , d ′ P + Q, d -→ P ′ , d ′ R5 P, e ⊔ ∃ x d -→ P ′ , e ′ ⊔ ∃ x d ∃ e x P, d -→ ∃ e ′ x P ′ , d ⊔ ∃ x e ′
From the internal point of view, the variable x, possibly occurring in the global store d, is hidden. This corresponds to the usual scoping rules: the x in d is global, hence "covered" by the local x. Therefore, P has no access to the information on x in d, and this is achieved by filtering d with ∃ x . Furthermore, P can use the information (which may also concern the local x) that has been produced locally and accumulated in e. In conclusion, if the visible store at the external level is d, then the store that is visible internally by P is e ⊔ ∃ x d. Now, if P is able to make a step, thus reducing to P ′ and transforming the local store into e ′ , what we see from the external point of view is that the process is transformed into ∃ e ′ x P ′ , and that the information ∃ x e present in the global store is transformed into ∃ x e ′ . To show how this works we show an instructive example.

R2 R5

(x > 10) ⊑ e ⊔ ∃ x d = (x > 42 ⊔ ∃ x (x > 2)) ask (x > 10) → Q, e ⊔ ∃ x d -→ Q, e ⊔ ∃ x d P, d -→ ∃ e x Q, d ⊔ ∃ x e
Note that the x in d is hidden, by using existential quantification in the reduction obtained by Rule R2. This expresses that the x in d is different from the one bound by the local process. Otherwise the ask process ask (x > 10) → Q would not be executed since the guard is not entailed by the global store d. Rule R2 applies since (x > 10) ⊑ e ⊔ ∃ x d. Note that the free x in e ⊔ ∃ x d is hidden in the global store, i.e. d ⊔ ∃ x e, to indicate that is different from the global x.

Remark 3. Observe that any transition is generated either by a process tell(c) or by a process ask (c) → Q. We say that a process P is active in a transition t = γ -→ γ ′ if it generates such transition; i.e if there exist a derivation of t where R1 or R2 are used to produce a transition of the form P, d -→ γ ′′ . Barbed Semantics. The authors in [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF] introduced a barbed semantics for CCP. Barbed equivalences have been introduced in [START_REF] Milner | Barbed bisimulation[END_REF] for CCS, and have become the standard behavioral equivalences for formalisms equipped with unlabeled reduction semantics. Intuitively, barbs are basic observations (predicates) on the states of a system. In the case of CCP, barbs are taken from the underlying set Con 0 of the constraint system.

Definition 2 (Barbs

). A configuration γ = P, d is said to satisfy the barb c (γ ↓ c ) iff c ⊑ d. Similarly, γ satisfies a weak barb c (γ ⇓ c ) iff there exist γ ′ s.t. γ -→ * γ ′ ↓ c .
To explain this notion consider the following example.

Example 3. Consider the constraint system from Example 1 and let

Var = {x}. Let γ = ask (x > 10) → tell(x > 42), x > 10 . We have γ ↓ x>5 since (x > 5) ⊑ (x > 10) and γ ⇓ x>42 since γ -→ tell(x > 42), x > 10 -→ stop, (x > 42) ↓ x>42 .
In this context, the equivalence proposed is the saturated bisimilarity [START_REF] Bonchi | Saturated semantics for reactive systems[END_REF][START_REF] Bonchi | Reactive systems, barbed semantics, and the mobile ambients[END_REF]. Intuitively, in order for two states to be saturated bisimilar, then (i) they should expose the same barbs, (ii) whenever one of them moves then the other should reply and arrive at an equivalent state (i.e. follow the bisimulation game), (iii) they should be equivalent under all the possible contexts of the language. In the case of CCP, it is enough to require that bisimulations are upward closed as in condition (iii) below.

Definition 3 (Saturated Barbed Bisimilarity). A saturated barbed bisimulation is a symmetric relation R on configurations s.t. whenever

(γ 1 , γ 2 ) ∈ R with γ 1 = P, c and γ 2 = Q, d implies that: (i) if γ 1 ↓ e then γ 2 ↓ e , (ii) if γ 1 -→ γ ′ 1 then there exists γ ′ 2 s.t. γ 2 -→ γ ′ 2 and (γ ′ 1 , γ ′ 2 ) ∈ R, (iii) for every a ∈ Con 0 , ( P, c ⊔ a , Q, d ⊔ a ) ∈ R.
We say that γ 1 and γ 2 are saturated barbed bisimilar (γ 1 ∼sb γ 2 ) if there exists a saturated barbed bisimulation R s.t. (γ 1 , γ 2 ) ∈ R.

We use the term "saturated" to be consistent with the original idea in [START_REF] Bonchi | Saturated semantics for reactive systems[END_REF][START_REF] Bonchi | Reactive systems, barbed semantics, and the mobile ambients[END_REF]. However, "saturated" in this context has nothing to do with the Milner's "saturation" for weak bisimilarity. In the following, we will continue to use "saturated" and "saturation" to denote these two different concepts.

Example 4. Consider the constraint system from Example 1 and let Var = {x}. Take P = ask (x > 5) → stop and Q = ask (x > 7) → stop. One can check that P ∼sb Q since P, x > 5 -→, while Q, x > 5 -→. Then consider P + Q, true and observe that P + Q, true ∼sb P, true . Indeed, for all constraints e, s.t. x > 5 ⊑ e, both the configurations evolve into stop, e , while for all e s.t. x > 5 ⊑ e, both configurations cannot proceed. Since x > 5 ⊑ x > 7, the behavior of Q is somehow absorbed by the behavior of P .

As we mentioned before, we are interested in deciding the weak version of the notion above. Then, weak saturated barbed bisimilarity ( ≈sb ) is obtained from Definition 3 by replacing the strong barbs in condition (i) for its weak version (⇓) and the transitions in condition (ii) for the reflexive and transitive closure of the transition relation (-→ * ). Formally, Definition 4 (Weak Saturated Barbed Bisimilarity). A weak saturated barbed bisimulation is a symmetric relation R on configurations s.t. whenever (γ 1 , γ 2 ) ∈ R with γ 1 = P, c and γ 2 = Q, d implies that:

(i) if γ 1 ⇓ e then γ 2 ⇓ e , (ii) if γ 1 -→ * γ ′ 1 then there exists γ ′ 2 s.t. γ 2 -→ * γ ′ 2 and (γ ′ 1 , γ ′ 2 ) ∈ R, (iii) for every a ∈ Con 0 , ( P, c ⊔ a , Q, d ⊔ a ) ∈ R.
We say that γ 1 and γ 2 are weak saturated barbed bisimilar (γ 1 ≈sb γ 2 ) if there exists a weak saturated barbed bisimulation R s.t. (γ 1 , γ 2 ) ∈ R.

To better understand this definition, consider the following example.

LR1 tell(c),

d true -→ stop, d ⊔ c LR2 α ∈ min{a ∈ Con 0 | c ⊑ d ⊔ a } ask (c) → P, d α -→ P, d ⊔ α LR3 P, d α -→ P ′ , d ′ P Q, d α -→ P ′ Q, d ′ LR4 P, d α -→ P ′ , d ′ P + Q, d α -→ P ′ , d ′ LR5 P [z/x], e[z/x] ⊔ d α -→ P ′ , e ′ ⊔ d ⊔ α ∃ e x P, d α -→ ∃ e ′ [x/z] x P ′ [x/z], ∃ x (e ′ [x/z]) ⊔ d ⊔ α with x ∈ fv (e ′ ), z ∈ fv (P ) ∪ fv (e ⊔ d ⊔ α)
Table 3: Labeled semantics for CCP (symmetric rules for LR3 and LR4 are omitted).

Example 5. Consider P and Q as in Example 4. We shall prove that P ≈sb Q. First notice that P, true -→ and also Q, true -→. Moreover, since none of the processes has the ability of adding information to the store, then for all a ∈ Con 0 , P, a ⇓ e iff e ⊑ a iff Q, a ⇓ e . Recall from Example 4 that P ∼sb Q since an observer can plug P into x > 5 and observe a reduction, which cannot be observed with Q. Instead P ≈sb Q since, intuitively, the discriminating power of ≈sb cannot observe any reductions.

Labeled Semantics

As explained in [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF], in a transition of the form P, d α -→ P ′ , d ′ the label α represents a minimal information (from the environment) that needs to be added to the store d to evolve from P, d into P ′ , d ′ , i.e., P, d ⊔ α -→ P ′ , d ′ . As a consequence, the transitions labeled with the constraint true are in one to one correspondence with the reductions defined in the previous section. For this reason, hereafter we will sometimes write -→ to mean true -→. Before formally introducing the labeled semantics, we fix some notation. Notation 1. We will use to denote a generic transition relation on the state space Conf and labels Con 0 . Also in this case mean true . Also, given a set of initial configurations IS , we shall use Config (IS ) to denote the set of reachable configurations3 using , i.e.:

Config (IS ) = {γ ′ | ∃γ ∈ IS s.t. γ α 1 . . . αn γ ′ for some n ≥ 0}
The LTS (Conf , Con 0 , -→) is defined by the rules in Table 3. The rule LR2, for example, says that ask (c) → P, d can evolve to P, d ⊔ α if the environment provides a minimal constraint α that added to the store d entails c, i.e., α ∈ min{a ∈ Con 0 | c ⊑ d ⊔ a}. Note that assuming that (Con, ⊑) is well-founded (Remark 1) is necessary to guarantee that α exists whenever {a ∈ Con 0 | c ⊑ d ⊔ a} is not empty. The rule LR5 in Table 3 uses in the antecedent derivation a fresh variable z that acts as a substitute for the free occurrences of x in P and its local store e. (Recall that T [z/x] represents T with x replaced with z). This way we identify with z the free occurrences of x in P and e and avoid clashes with those in α and d. The other rules are easily seen to realize the intuition given in Section 2.2.2. Figure 2 illustrates the LTSs of our running example.

To better understand the labeled semantics consider the following example. The labeled semantics is sound and complete w.r.t. the unlabeled one. Soundness states that P, d α -→ P ′ , d ′ corresponds to our intuition that if α is added to d, P can reach P ′ , d ′ . Completeness states that if we add a to (the store in) P, d and reduce to P ′ , d ′ , it exists a minimal information α ⊑ a such that P, d

α -→ P ′ , d ′′ with d ′′ ⊑ d ′ .
The following lemma is an extension of the one in [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF] which considers nondeterministic CCP. x > 70

T = tell(true) T ′ = tell(x > 100) P = ask (x > 70) → T S = ask (x > 7) → P Q = ask (x > 50) → T Q ′ = ask (x > 50) → T ′ R = ask (x > 5) → (P + Q) R ′ = ask (x > 5) → (P + Q ′ ) R + S, true S, true R ′ + S, true P + Q ′ , x
x > 5

x > 7

x > 7

x > 5

x > 7

x > 50

x > 70

x > 50

x > 70 • Using Rule LR4 (Table 3), take P = Q + R and

P ′ = Q ′ then we have Q, d α -→ Q ′ , d ′ by a shorter inference. By appeal to induction then Q, d ⊔ α -→ Q ′ , d ′ . Applying Rule R4 (Table 2) to the previous reduc- tion we get Q + R, d ⊔ α -→ Q ′ , d ′ .
(Completeness) The proof proceeds by induction on (the depth) of the inference of P, d⊔a -→ P ′ , d ′ . Again, we consider only the case for the non-deterministic choice.

• Using Rule R4 (Table 2), take The above lemma is central for deciding bisimilarity in CCP. In fact, we will show later that, for the weak (saturated) semantics, the completeness direction does not hold. From this we will show that the standard reduction from weak to strong does not work.

P = Q + R and P ′ = Q ′ then we have Q, d ⊔ a -→ Q ′ ,

Deciding strong bisimilarity for CCP

In this section we recall how to check ∼sb with a modified version of partition refinement introduced in [START_REF] Aristizábal | Partition refinement for bisimilarity in CCP[END_REF]. Henceforth, we shall refer to this algorithm as CCP partition refinement.

Equivalences: Saturated Barbed, Irredundant and Symbolic Bisimilarity

The main problem with checking ∼sb is the quantification over all contexts. This problem is addressed in [START_REF] Aristizábal | Partition refinement for bisimilarity in CCP[END_REF] following the abstract approach in [START_REF] Bonchi | Minimization algorithm for symbolic bisimilarity[END_REF]. More precisely, we use an equivalent notion, namely irredundant bisimilarity ∼I , which can be verified with CCP partition refinement. As its name suggests, ∼I only takes into account those transitions deemed irredundant. However, technically speaking, going from ∼sb to ∼I requires one intermediate notion, so-called symbolic bisimilarity. These three notions are shown to be equivalent, ∼sb = ∼sym = ∼I . In the following we recall all of them.

Let us first give some auxiliary definitions. Unlike for the standard partition refinement, we need to consider a particular kind of transitions, so-called irredundant transitions. These are those transitions that are not dominated by others, in a given partition, in the sense defined below.

Definition 5 (Transition Derivation). Let t and t ′ be two transitions of the form t = (γ, α, P ′ , c ′ ) and t ′ = (γ, β, P ′ , c ′′ ). We say that t derives t ′ , written t

⊢ D t ′ , iff α ⊑ β and c ′′ = c ′ ⊔ β.
The intuition is that the transition t dominates t ′ iff t requires less (or equal) information from the environment than t ′ does (hence α ⊑ β), and they end up in configurations which differ only by the additional information in β not present in α (hence c ′′ = c ′ ⊔ β). To better explain this notion let us give an example.

Example 7. Consider the following process:

P = (ask (x > 10) → tell(x > 42)) + (ask (x > 15) → tell(x > 42))
and let γ = P, true . Now let t 1 and t 2 be transitions defined as:

t 1 = γ x>10 -→ tell(x > 42), x > 10 and t 2 = γ x>15 -→ tell(x > 42), x > 15 One can check that t 1 ⊢ D t 2 since (x > 10) ⊑ (x > 15) and also (x > 15) = ((x > 15) ⊔ (x > 10)).
Notice that in the definition above t and t ′ end up in configurations whose processes are syntactically identical (i.e., P ′ ). The following notion parameterizes the notion of dominance w.r.t. a relation on configurations R (rather than fixing it to the identity on configurations). Definition 6 (Transition Derivation w.r.t. R). We say that the transition t derives a transition t ′ w.r.t a relation on configurations R, written t ⊢ R t ′ , iff there exists t ′′ such that t ⊢ D t ′′ , lab(t ′′ ) = lab(t ′ ) and tar (t ′′ )R tar (t ′ ). 4To better understand this definition consider the following example.

Example 8. Consider the following processes:

Q 1 = (ask (b) → (ask (c) → tell(d))) and Q 2 = (ask (a) → stop) Now let P = Q 1 + Q 2 where d ⊑ c and a ⊏ b.
Then take γ = P, true and consider the transitions t and t ′ as:

t = γ a -→ stop, a and t ′ = γ b -→ ask (c) → tell(d), b
Finally, let R = ≈sb and take t ′′ = (γ, b, stop, b ) which is constructed using the target process in t and the label in t ′ . One can check that t ⊢ R t ′ as in Definition 8. Firstly, t ⊢ D t ′′ follows from a ⊏ b. Secondly, we know tar (t ′′ )R tar (t ′ ) from Example 6, i.e. stop, b ≈sb ask (c) → tell(d), b since stop, true ≈sb ask (c) → tell(d), true . Now we introduce the concept of domination, which consists in strengthening the notion of derivation by requiring labels to be different. Definition 7 (Transition Domination). Let t and t ′ be two transitions of the form t = (γ, α, P ′ , c ′ ) and t ′ = (γ, β, P ′ , c ′′ ). We say that t dominates t ′ , written t ≻ D t ′ , iff t ⊢ D t ′ and α = β.

As we did for derivation, we now parameterize the notion of domination as follows.

Definition 8 (Transition Domination w.r.t. R and Irredundant Transition w.r.t. R). We say that the transition t dominates a transition t ′ w.r.t a relation on configurations R, written t ≻ R t ′ , iff there exists t ′′ such that t ≻ D t ′′ , lab(t ′′ ) = lab(t ′ ) and tar (t ′′ )R tar (t ′ ). A transition is said to be redundant w.r.t. to R when it is dominated by another w.r.t. R, otherwise it is said to be irredundant w.r.t. to R.

We are now able to introduce symbolic bisimilarity. Intuitively, two configurations γ 1 and γ 2 are symbolic bisimilar iff (i) they have the same barbs and (ii) whenever there is a transition from γ 1 α -→ γ ′ 1 , then we require that γ 2 must reply with a similar transition γ 2 α -→ γ ′ 2 (where γ ′ 1 and γ ′ 2 are now equivalent) or some other transition that derives it. In other words, the move from the defender does not need to use exactly the same label, but a transition that is "stronger" (in terms of derivation ⊢ D ) could also do the job. Formally we have the definition below.

Definition 9 (Symbolic Bisimilarity). A symbolic bisimulation is a symmetric relation R on configurations s.t. whenever

(γ 1 , γ 2 ) ∈ R with γ 1 = P, c and γ 2 = Q, d implies that: (i) if γ 1 ↓ e then γ 2 ↓ e , (ii) if P, c α -→ P ′ , c ′ then there exists a transition t = Q, d β -→ Q ′ , d ′′ and a store d ′ s.t. t ⊢ D Q, d α Q ′ , d ′ and P ′ , c ′ R Q ′ , d ′ .
We say that γ 1 and γ 2 are symbolic bisimilar (γ 1 ∼sym γ 2 ) if there exists a symbolic bisimulation R s.t. (γ 1 , γ 2 ) ∈ R.

Let us illustrate the definition above by using the process in Figure 2.

Example 9. Consider the following processes:

T = tell(true), P = ask (x > 5) → T and Q = ask (x > 7) → T
We provide a symbolic bisimulation R = {( P + Q, true , P, true )} ∪ id to prove P + Q, true ∼sym P, true . Take the pair ( P + Q, true , P, true ).

The first condition in Definition 9 is trivial. As for the second one, let us take the transition P + Q, true x>7 -→ T, x > 7 . We have to check that P, true is able to reply with a stronger transition. Thus consider the transitions t and t ′ as follows:

t = P, true x>5 -→ T, x > 5 and t ′ = P, true x>7 T, x > 7
Then we can observe that t ⊢ D t ′ and T, x > 7 R T, x > 7 . The remaining pairs are trivially verified.

And finally, the irredundant version, which follows the standard bisimulation game where labels need to be matched, however only those so-called irredundant transitions must be considered.

Definition 10 (Irredundant Bisimilarity). An irredundant bisimulation is a symmetric relation R on configurations s.t. whenever

(γ 1 , γ 2 ) ∈ R implies that: (i) if γ 1 ↓ e then γ 2 ↓ e , (ii) if γ 1 α -→ γ ′ 1 and it is irredundant in R then there exists γ ′ 2 s.t. γ 2 α -→ γ ′ 2 and (γ ′ 1 , γ ′ 2 ) ∈ R.
We say that γ 1 and γ 2 are irredundant bisimilar (γ

P + Q, true x>5 -→ T, x > 5 ≻ R P + Q, true x>7 -→ T, x > 7 hence P + Q, true x>7 -→ T, x > 7 is redundant since (x > 5) ⊏ (x > 7)
, therefore it does not need to be matched by P, true .

As we said at the beginning, the above-defined equivalences coincide with saturated barbed bisimilarity ( ∼sb , Definition 3). The proof, given in [START_REF] Aristizábal | Partition refinement for bisimilarity in CCP[END_REF], strongly relies on Lemma 1.

Theorem 1 ([12]). P, c ∼I Q, d iff P, c ∼sym Q, d iff P, c ∼sb Q, d
Using this theorem we can define a modified partition refinement, that consider only the irredundant transitions, in order to compute ∼sb as we shall see in the next section.

Partition Refinement for CCP

In [START_REF] Aristizábal | Partition refinement for bisimilarity in CCP[END_REF] we adapted the standard partition refinement procedure to decide strong bisimilarity for CCP ( ∼sb ). As we did for the standard partition refinement, we start with Config -→ (IS ), that is the set of all states that are reachable from the set of initial state IS using -→. However, in the case of CCP some other states must be added to IS ⋆ in order to verify ∼sb as we will explain later on.

First, since configurations satisfying different barbs are surely different, the algorithm can be safely started with a partition that equates each state satisfying the same barbs. Hence, as initial partition of IS ⋆ , we take P 0 = {B 1 } . . . {B m }, where γ and γ ′ are in B i iff they satisfy the same barbs.

We now explain briefly how to compute IS ⋆ using the Rules in Table 4. Rules (IS IS ) and (RS IS ) say that all the reachable states using the transition relation from the set of initial states should be included, i.e., Config (IS ) ⊆ IS ⋆ .

The rule (RD IS ) adds the additional states needed to check redundancy. Consider the transitions

t 1 = γ α P 1 , c 1 and t 2 = γ β P 2 , c 2 with α ⊏ β and c 2 = c 1 ⊔ β in Rule (RD IS )
. Suppose that at some iteration of the partition refinement algorithm the current partition is P and that P 2 , c 2 P P 1 , c 2 . Then, according to Definition 8 the transitions t 1 would dominate t 2 w.r.t P. This makes t 2 redundant w.r.t P. Since P 1 , c 2 may allow us to witness a potential redundancy of t 2 , we include it in IS ⋆ (and thus, from the definition of the initial

(IS IS ) γ ∈ IS γ ∈ IS ⋆ (RS IS ) γ ∈ IS ⋆ γ α γ ′ γ ′ ∈ IS ⋆ (RD IS ) γ ∈ IS ⋆ t 1 = γ α P 1 , c 1 t 2 = γ β P 2 , c 2 α ⊏ β c 2 = c 1 ⊔ β P 1 , c 2 ∈ IS ⋆
Table 4: Rules for generating the states used in the partition refinement for ccp partition P 0 , also in the block of P 0 where P 2 , c 2 is). See [START_REF] Aristizábal | Partition refinement for bisimilarity in CCP[END_REF] for further details about the computation of IS ⋆ . Finally, instead of using the function F (P) of Algorithm 1, the partitions are refined by employing the function IR (P) defined as follows: Definition 11. (Refinement function for CCP) Given a partition P we define IR (P) as follows:

γ 1 IR (P) γ 2 iff if γ 1 α γ ′ 1 is irredundant w.r.t. P then there exists γ ′ 2 s.t. γ 2 α γ ′ 2 and γ ′ 1 Pγ ′ 2
Using this function, the partition refinement algorithm for CCP is defined as follows:

Algorithm 2 pr-ccp(IS , ) Initialization 1. Compute IS ⋆ with the rules (IS IS ), (RS IS ), (RD IS ) defined in Table 4, Algorithm 2 can be used to decide ∼sb with exponential time whenever the set of reachable states is finite. (Recall that Config -→ (IS ) represents the set of states that are reachable from the initial states IS using -→.) More precisely: Theorem 2. ( [START_REF] Aristizábal | Partition refinement for bisimilarity in CCP[END_REF]) Let γ and γ ′ be two CCP configurations. Let IS = {γ, γ ′ } and let P be the output of pr-ccp(IS , -→) in Algorithm 2. If Config -→ (IS ) is finite then:

2. P 0 = {B 1 } . . . {B m }
• γ P γ ′ iff γ ∼sb γ ′ .
• pr-ccp(IS , -→) may take exponential time in the size of Config -→ (IS ).

The exponential time is due to construction of the set IS ⋆ -→ (Algorithm 2, step 1) whose size is exponential in |Config -→ (IS )|.

Incompleteness of Milner's saturation method in CCP

As mentioned at the beginning of this section, the standard approach for deciding weak equivalences is to add some transitions to the original processes, socalled saturation, and then check for the strong equivalence. In calculi like CCS, such saturation consists in forgetting about the internal actions that make part of a sequence containing one observable action (Table 5). However, for CCP this method does not work. The problem is that the transition relation proposed by Milner is not complete for CCP, hence the relation among the saturated, symbolic and irredundant equivalences is broken. In the next section we will provide a stronger saturation, which is complete, and allows us to use the CCP partition refinement to compute ≈sb .

Let us show why Milner's approach does not work. First, we need to introduce formally the concept of completeness for a given transition relation. Notice that -→ (i.e the reduction semantics, see Table 2) is complete, and it corresponds to the second item of Lemma 1. Now Milner's method defines a

Definition 12 (Completeness). We say that is complete if and only if whenever

MR1 γ α -→ γ ′ γ α =⇒ γ ′ MR2 γ =⇒ γ MR3 γ =⇒ γ 1 α =⇒ γ 2 =⇒ γ ′ γ α =⇒ γ ′ Table 5: Milner's Saturation Method for CCP ask α → (ask β → stop), α ⊔ β ask β → stop, α ⊔ β stop, α ⊔ β ask α → (ask β → stop), true ask β → stop, α stop, α ⊔ β α β missing α ⊔ β
Figure 3: Counterexample for completeness using Milner's saturation method (cycles from MR2 omitted). Both graphs are obtained using Table 5.

new transition relation =⇒ using the rules in Table 5, but it turns out not to be complete.

Proposition 1. The relation =⇒ defined in Table 5 is not complete.

Proof. We will show a counter-example where the completeness for =⇒ does not However, notice that the only transition possible is P, true α =⇒ (ask β → stop), α , hence completeness does not hold since there is no transition from P, true to stop, c ′′ for some c ′′ . Figure 3 illustrates the problem.

We can now use this fact to see why the method does not work for computing ≈sb using CCP partition refinement. First, let us redefine some concepts using the new transition relation =⇒. Because of condition (i) in ≈sb , we need a new definition of barbs, namely weak barbs w.r.t. =⇒. Definition 13. We say γ satisfies a weak barb e w.r.t. =⇒, written γ e , if and only if γ =⇒ * γ ′ ↓ e .

We shall see later on that coincides with ⇓. Using this notion, we introduce symbolic and irredundant bisimilarity w.r.t. =⇒, denoted by ∼=⇒ sym and ∼=⇒ I respectively. They are defined as in Definition 9 and 10 where in condition (i) weak barbs (⇓) are replaced with and in condition (ii) the transition relation is now =⇒. More precisely: Definition 14 (Symbolic Bisimilarity over =⇒). A symbolic bisimulation over =⇒ is a symmetric relation R on configurations s.t. whenever (γ 1 , γ 2 ) ∈ R with γ 1 = P, c and γ 2 = Q, d :

(i) if γ 1 e then γ 2 e , (ii) if P, c α =⇒ P ′ , c ′ then there exists a transition t = Q, d β =⇒ Q ′ , d ′′ s.t. t ⊢ D Q, d α Q ′ , d ′ and P ′ , c ′ R Q ′ , d ′
We say that γ 1 and γ 2 are symbolic bisimilar over =⇒, written γ 1 ∼=⇒ sym γ 2 , if there exists a symbolic bisimulation over =⇒ s.t. (γ 1 , γ 2 ) ∈ R.

Definition 15 (Irredundant Bisimilarity over =⇒). An irredundant bisimulation over =⇒ is a symmetric relation R on configurations s.t. whenever (γ 1 , γ 2 ) ∈ R:

(i) if γ 1 e then γ 2 e , (ii) if γ 1 α =⇒ γ ′ 1 and it is irredundant in R then there exists γ ′ 2 s.t. γ 2 α =⇒ γ ′ 2 and (γ ′ 1 , γ ′ 2 ) ∈ R.
We say that γ 1 and γ 2 are irredundant bisimilar over =⇒, written γ 1 ∼=⇒

I γ 2 , if there exists an irredundant bisimulation over =⇒ s.t. (γ 1 , γ 2 ) ∈ R.
One would expect that since ∼sb = ∼sym = ∼I then it is the case that ≈sb = ∼=⇒ sym = ∼=⇒ I , given that these new notions are supposed to be the weak versions of the former ones when using the saturation method. However, completeness is necessary for proving ∼sb = ∼sym = ∼I , and from Proposition 1 we know that =⇒ is not complete hence we might expect that ≈sb does not imply ∼=⇒ sym nor ∼=⇒ I . In fact, the following counter-example proves this. Example 11. Let P, P ′ and Q as in Figure 4 and5. Let IS = { P, true , Q, true } Figure 4 shows LTS -→ (IS ). Figure 5 presents LTS =⇒ (IS ) where =⇒ is defined in Table 5 (Milner's saturation method).

First, notice that P, true ≈sb Q, true , since there exists a saturated weak barbed bisimulation: R = {( P, true , Q, true )} ∪ id However, P, true ∼=⇒ I Q, true . To prove that, we need to pick an irredundant transition from P, true or Q, true (after saturation) s.t. the other cannot match. Thus, take Q, true α⊔β -→ tell(c), α ⊔ β which is irredundant and given that P, true does not have a transition labeled with α ⊔ β then we know that we cannot find an irredundant bisimulation containing ( P, true , Q, true ) therefore P, true ∼=⇒ I Q, true . Using the same reasoning we can also show that ≈sb does not imply ∼=⇒ sym .

P = ask (α) → P ′ P ′ = (ask (β) → tell(c)) + (ask (true) → tell(d)) P, true P ′ , α tell(d), α tell(c), α ⊔ β stop, α ⊔ β ⊔ c stop, α ⊔ d α β Q = P + (ask (α ⊔ β) → tell(c)) Q, true P ′ , α tell(d), α tell(c), α ⊔ β stop, α ⊔ β ⊔ c stop, α ⊔ d α β α ⊔ β Figure 4: LTS -→ ({ P, true , Q, true })

Reducing weak bisimilarity to Strong in CCP

In this section we shall provide a method for deciding weak bisimilarity in CCP. As shown in Section 2.4, the usual method for deciding weak bisimilarity (introduced in Section 2.1) does not work for CCP. We shall proceed by redefining =⇒ in such a way that it is sound and complete for CCP. Then we prove that, w.r.t. =⇒, symbolic and irredundant bisimilarity coincide with ≈sb , i.e. ≈sb = ∼=⇒ sym = ∼=⇒ I . We therefore conclude that the partition refinement algorithm in [START_REF] Aristizábal | Partition refinement for bisimilarity in CCP[END_REF] can be used to verify ≈sb w.r.t. =⇒.

Defining a new saturation method for CCP

If we analyze the counter-example to completeness (see Figure 3), one can see that the problem arises because of the nature of the labels in CCP, namely using this method ask α → (ask β → stop), true does not have a transition with α ⊔ β to stop, α ⊔ β , hence that fact can be exploited to break the relation among the weak equivalences. Following this reasoning, instead of only forgetting about the silent actions we also take into account that labels in CCP can be added together. Thus we have a new rule that creates a new transition for each two consecutive ones, whose label is the lub of the labels in them. This method can also be thought as the reflexive and transitive closure of the labeled transition relation α -→. Such transition relation turns out to be sound and complete and it can be used to decide ≈sb .

The remaining part of this section is structured as follows. First we define a new saturation method and we proceed to prove that the weak barbs resulting

P = ask (α) → P ′ P ′ = (ask (β) → tell(c)) + (ask (true) → tell(d)) P, true P ′ , α tell(d), α tell(c), α ⊔ β stop, α ⊔ β ⊔ c stop, α ⊔ d α β α α β Q = P + (ask (α ⊔ β) → tell(c)) Q, true P ′ , α tell(d), α tell(c), α ⊔ β stop, α ⊔ β ⊔ c stop, α ⊔ d α β α ⊔ β α α β Figure 5: LTS =⇒ ({ P, true , Q, true })
where =⇒ is defined in Table 5 (Milner's saturation method). The cycles from rule MR2 are omitted. The dashed transitions are those added by the rules in Table 5. The dotted transition is the (irredundant) one that Q, true can take but P, true cannot match, therefore showing that P, true ∼=⇒ I Q, true from such method are consistent with that of CCP (as in Definition 2). Then under the assumption that -→ is finitely branching we prove that =⇒ is also finitely branching. Moreover, we follow by showing how this method would be inaccurate in CCS-like formalisms since it could turn a finitely branching LTS into be infinitely branching one. With these elements we can prove soundness and completeness, which can be finally used to prove the correspondence among ≈sb , ∼=⇒ sym and ∼=⇒ I .

A new saturation method

Formally, our new transition relation =⇒ is defined by the rules in Table 6.

Remark 4. For simplicity, we shall use the same notation (=⇒) we used for Milner's method (Table 5) to denote the new saturation method ( First we show that coincides with ⇓ since a transition in =⇒ corresponds to a sequence of reductions. 5Lemma 2. γ -→ * γ ′ iff γ =⇒ γ ′ .

R-Tau γ =⇒ γ R-Label γ α -→ γ ′ γ α =⇒ γ ′ R-Add γ α =⇒ γ ′ β =⇒ γ ′′ γ α⊔β =⇒ γ ′′
Proof. (⇒) We can decompose γ -→ * γ ′ as follows γ -→ γ 1 -→ . . . -→ γ i -→ γ ′ , now we proceed by induction on i. The base case is i = 0, then γ -→ γ ′ and by rule R-Label we have γ =⇒ γ ′ . For the inductive step, first we have by induction hypothesis that γ -→ i γ i implies γ =⇒ γ i (1), on the other hand, by rule R-Label on γ i -→ γ ′ we can deduce γ i =⇒ γ ′ (2). Finally by R-Add on ( 1) and ( 2) γ =⇒ γ ′ .

(⇐) We proceed by induction on the depth of the inference of γ =⇒ γ ′ . First, using R-Tau, we can directly conclude γ -→ * γ. Secondly, using R-Label, γ =⇒ γ ′ implies that γ -→ γ ′ . Finally, using R-Add and since α ⊔ β = true implies α = β = true, we get γ =⇒ γ ′′ =⇒ γ ′ and by induction hypothesis this means that γ -→ * γ ′′ -→ * γ ′ therefore γ -→ * γ ′ .

Using this lemma, it is straightforward to see that the notions of weak barbs coincide. 6Lemma 3. γ ⇓ e iff γ e .

Proof. First, let us assume that γ ⇓ e then by definition γ -→ * γ ′ ↓ e , and from Lemma 2 we know that γ =⇒ γ ′ ↓ e , hence γ e . On the other hand, if γ e then by definition γ =⇒ * γ ′ ↓ e , if we decompose these transitions then γ =⇒ . . . =⇒ γ ′ , and from Lemma 2 γ -→ * . . . -→ * γ ′ , therefore γ -→ * γ ′ ↓ e , finally γ ⇓ e .

As we shall see later on, the lemma above will be used to prove the correspondence between ≈sb and ∼=⇒ I .

The new saturation method is finitely branching

An important property that the labeled transition system defined by the new relation =⇒ must fulfill is that it must be finitely branching, given that -→ is also finitely branching. We prove this next but first let us introduce some useful notation.

The set Reach(γ, ), defined below, represents the set of configurations which results after performing one step starting from a given configuration γ and using a relation . Such set contains pairs of the form [γ ′ , α] in which the first item (γ ′ ) is the configuration reached and the second one (α) is the label used for that purpose. Formally we have: Definition 16 (Single-step Reachable Pairs). The set of Single-step reachable pairs is defined as Reach(γ,

) = {[γ ′ , α] | γ α γ ′ }.
We can extend this definition to consider more than one step at a time. We will call this new set Reach * (γ, ) and it is defined below.

Definition 17 (Reachable Pairs). The set of reachable pairs is defined as follows:

Reach * (γ, ) = {[γ ′ , α] | ∃α 1 , . . . , α n . γ α 1 . . . αn γ ′ ∧ α = α n }.
Using the notation defined above, we shall define formally what we mean by finitely branching as follows.

Definition 18. We say that a transition relation is finitely branching if for all γ we have |Reach(γ, )| < ∞.

Remark 5. It is worth noticing that even though we have restricted the syntax of ccp to finite processes, for some constraint systems -→ may be infinitelybranching due to Rule LR2 in Table 3; i.e., there may be infinitely many minimal labels allowing the transition. For this reason we shall sometimes explicitly assume that -→ is defined in constraint systems that do not cause -→ to be infinitely-branching.

For convenience, in order to project the first or the second item of the reachable pairs we will define the functions C and L which, respectively, extract the configuration and the label respectively (hence the name).

A Remark about our Saturation in CCS

We assume that the reader is familiar with CCS [START_REF] Milner | A Calculus of Communicating Systems[END_REF]. In this section the transitions, processes and relations are understood in the context of CCS. It is worth noticing that we could use the saturation method mentioned in the previous section for other formalisms like CCS, but unlike in CCP it would not work as intended: now, the actions that a process can perform need to be sequences and the rules in Using these rules we can now define weak bisimilarity in terms of the new relation =⇒ CCS as follows.

Definition 20 (CCS-Weak Bisimilarity). A symmetric relation R is a CCS-weak bisimulation if for every (P, Q) ∈ R:

• If P s =⇒ CCS P ′ then there exists Q ′ s.t. Q s =⇒ CCS Q ′ and (P ′ , Q ′ ) ∈ R.
We say that P and Q are CCS-weakly bisimilar (P ≈ Q) iff there is a CSS-weak bisimulation containing (P, Q).

This definition resembles the standard definition of strong bisimilarity, hence we could use the procedure to verify the strong version under =⇒ in order to verify the weak one. However, by applying the rules in Table 7, even for a finite LTS, we could end up adding an infinite number of transitions. The following example illustrates the problem. Example 12. Let us take a typical one-state finitely-branching CCS process with a single transition labeled with a into itself (See Figure 6-(a)). However, if we apply the rules in Table 7 for the example above, we end up adding an infinite number of transitions. Hence, becoming infinitely branching (see Figure 6-(b)).

Soundness and Completeness

As mentioned before, soundness and completeness of the relation are the core properties when proving ∼sb = ∼sym = ∼I . We now proceed to show that our method enjoys of these properties and they will allow us to prove the correspondence among the equivalences for the weak case.

Recall that in Definition 12 we introduced the formal definition of completeness, now we shall introduce the notion of soundness.

Definition 21 (Soundness). We say that is sound iff whenever P, c α P ′ , c ′ then P, c ⊔ α P ′ , c ′ .

Below we shall prove that =⇒ from Table 6 is sound and complete.

Lemma 6 (Soundness of =⇒). If P, c

α =⇒ P ′ , c ′ then P, c ⊔ α =⇒ P ′ , c ′ .
Proof. We proceed by induction on the depth of the inference of P, c α =⇒ P ′ , c ′ .

• Using R-Tau we have P, c =⇒ P, c and the result follows directly given that α = true.

• Using R-Label we have P, c α =⇒ P ′ , c ′ then P, c α -→ P ′ , c ′ . By Lemma 1 (soundness of -→) we get P, c ⊔ α -→ P ′ , c ′ and finally by rule R-Label P, c ⊔ α =⇒ P ′ , c ′ .

• Using R-Add then we have P, c Proof. Assuming that P, c⊔a =⇒ P ′ , c ′ then, from Lemma 2, we can say that P, c⊔a -→ * P ′ , c ′ which can be written as P, c⊔a -→ . . . -→ P i , c i -→ P ′ , c ′ , we will proceed by induction on i.

• (Base Case) Assuming i = 0 then P, c ⊔ a -→ P ′ , c ′ and the result follows directly from Lemma 1 (Completeness of -→) and R-Label.

•

Deciding Observational Equivalence

In this section we shall show our main result, a method for deciding ≈sb . Recall that ≈sb is the standard weak bisimilarity for CCP [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF], and it is defined in terms of -→, therefore it does not depend on =⇒. We start from the fact that using CCP partition refinement (Section 2.3.2) one can check whether two configurations are irredundant bisimilar ( ∼I ). Following the same approach, we prove that ≈sb = ∼=⇒ sym = ∼=⇒ I hence we give a reduction from ≈sb to ∼=⇒ I . Finally, ∼=⇒ I can be verified using a modified version of the CCP partition refinement (as we shall see in Section 4).

First, given that =⇒ is sound and complete (Lemma 6 and Lemma 7), the correspondence between the symbolic and irredundant bisimilarity follows from [START_REF] Aristizábal | Partition refinement for bisimilarity in CCP[END_REF].

Corollary 1. γ ∼=⇒ sym γ ′ iff γ ∼=⇒ I γ ′
Finally, in the next two lemmata, we prove that ≈sb = ∼=⇒ sym . Lemma 8. If γ ≈sb γ ′ then γ ∼=⇒ sym γ ′ Proof. We need to prove that R = {( P, c , Q, d ) | P, c ≈sb Q, d } is a symbolic bisimulation over =⇒. The first condition (i) of the bisimulation follows directly from Lemma 3. As for (ii), let us assume that P, c α =⇒ P ′ , c ′ then by soundness of =⇒ we have P, c ⊔ α =⇒ P ′ , c ′ , now by Lemma 2 we obtain P, c ⊔ α -→ * P ′ , c ′ . Given that P, c ≈sb Q, d then from the latter transition we can conclude that Q Using Lemma 8 and Lemma 9 we obtain the following theorem.

, d ⊔ α -→ * Q ′ , d ′ where P ′ , c ′ ≈sb Q ′ , d ′ ,
Theorem 3. P, c ∼=⇒ sym Q, d iff P, c ≈sb Q, d From the above results, we conclude that ≈sb = ∼=⇒ I .

Algorithm for observational equivalence in CCP

In this section we describe the decision procedure for verifying weak version of saturated bisimilarity ( ≈sb ). The approach is to reduce the problem of deciding ≈sb to that of deciding strong bisimilarity as illustrated in Figure 7. The latter problem can be decided using the partition refinement for CCP (Algorithm 2).

Figure 7: Summary of our approach More precisely, given two configurations γ and γ ′ , the first step is to build G = LTS -→ (IS ) where IS = {γ, γ ′ }. We proceed to compute G ′ = LTS =⇒ (IS ), and then run an adaptation of Algorithm 2 on G ′ . The adaptation consists in using weak barbs (⇓ c ) instead of barbs (↓ c ) for the initial partition P 0 , and in using =⇒ as a parameter of Algorithm 3.

Using this algorithm we can decide ≈sb also with exponential time as we shall see below. First, let us determine the complexity of computing LTS =⇒ (IS ). Proof. By construction of γ ′ the rules in Table 6 never add a new vertex, thus it follows directly that N ′ = N . As for the edges, the rules in Table 6 will add, at most, a transition from each element in V(G) to every other configuration in V(G). Since V(G) = N then the resulting transitions are M ′ = O(N 2 ). Proof. Let n > 0. We define P n = P n 0 with P n i , for i ∈ {0, . . . , n -1}, given by:

P n i = (ask b i → stop) + (ask a i → P n i+1 )
and P n n = tell(b n ). Furthermore, we assume that for all i ∈ {0, . . . , n -1} we have a i ⊏ b i and for all j ∈ {0, . . . , n -1} if i = j then a i ⊑ a j and b i ⊑ b j . The reachable states from P n , true are illustrated below. Notice that that size of the set of reachable states |Config -→ (IS )| is 2n. By using the rules (IS IS ), (RS IS ) and (RD IS ) in Table 4 with = =⇒ and also IS = { P n , true }, we obtain an IS ⋆ =⇒ whose size is given by the following recurrence relation, for n > 0: f (n) = 2f (n -1) + 2 with f (0) = 2. Without loss of generality consider the first level of transitions of P n , true : procedure in a better scenario in order to compare it with the strong version. We did this by randomly generating test cases fulfilling the linearity constraint.

Concluding Remarks

We showed that the weak transition relation using Milner's saturation method is not complete for CCP (in the sense of Definition 12). This implied that ≈sb (Definition 4, [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF]) cannot be computed immediately by using the CCP partition refinement algorithm for (strong) bisimilarity CCP on the saturated transition relation. We then introduced a new transition relation using a different saturation mechanism and showed that it is complete for CCP and also that it is finitely branching. As a consequence, we also showed that the CCP partition refinement can be used to compute ≈sb using this new relation. Likewise, we have shown that although this new saturation method elaborated for CCP could be used for any other formalisms such as CCS, it would not work as desired because it could transform a finitely branching LTS into an infinitely branching one. To the best of our knowledge, this is the first approach to verifying weak bisimilarity for CCP. As future work, we plan to adapt and implement our notion of (weak) bisimilarity for variants of CCP, in particular for Spatial CCP [START_REF] Knight | Spatial and epistemic modalities in constraint-based process calculi[END_REF]. This calculus is a meaningful extension of CCP for modeling spatially distributed concurrent systems such as social networks. The spatial and hierarchical aspects of this variant may offer challenges for the theoretical and practical aspects of a weak bisimulation semantics.

Example 2 .

 2 Consider the constraint system from Example 1 and let Var = {x}. Let P = ∃ e x (ask (x > 10) → Q) with local store e = x > 42, and global store d = x > 2.

Example 6 . 2 c-

 62 Let γ 1 = tell(true), true and γ 2 = ask (c) → tell(d), true . We can show that γ 1 ≈sb γ 2 when d ⊑ c. Intuitively, this corresponds to the fact that the implication c ⇒ d is equivalent to true when c entails d. Note that LTS -→ (γ 1 ) and LTS -→ (γ 2 ) are the following: γ 1 -→ stop, true and γ → tell(d), c -→ stop, c . Consider now the relation R as follows: R = {(γ 2 , γ 1 ), (γ 2 , stop, true ), ( tell(d), c , stop, c ), ( stop, c , stop, c )} One can verify that the symmetric closure of R is a weak saturated barbed bisimulation as in Definition 3.

> 5 P, x > 7 P + Q, x > 5 P, x > 5 T

 5755 ′ , x > 50 T, x > 70 T, x > 50 T, x > 70 stop, x > 100 stop, x > 70 stop, x > 50 stop, x > 70

Figure 2 :

 2 Figure 2: LTS -→ ({ R ′ + S, true , S, true , R + S, true , P, x > 5 }).

  d ′ by a shorter inference. Note that the active process generating the transition could be either an ask or a tell (See Remark 3). Let suppose that the constraint that has been either asked or told is c. If it is generated by an ask then d ′ = d ⊔ a and c ⊑ d ⊔ a. Note that a ∈ {a ′ ∈ C on 0 |c ⊑ d ⊔ a ′ }, and then by Remark 1 there exists α ∈ min({a′ ∈ Con 0 |c ⊑ d ⊔ a ′ }) such that α ⊑ a. If it is generated by a tell then d ′ = d ⊔ a ⊔ c, thus in both cases is safe to assume that d ′ = d ⊔ a ⊔ c.Thereafter by induction hypothesis we have that there exist α and b such that:Q, d α -→ Q ′ , d ′′with a = α⊔b and d ′ = d ′′ ⊔b. As said formerly the active process generating this transition could be either an ask or a tell. If it is generated by an ask then d ′′ = d ⊔ α and if it is generated by a tell then α = true and d ′′ = d ⊔ c. Hence in both cases is safe to assume that d ′′ = d ⊔ c. Now by Rule LR4 we have that Q + R, d α -→ Q ′ , d ′′ since d ′′ = d⊔c we say that a = b and that d ′ = d⊔a⊔c = d⊔b⊔c = d ′′ ⊔b.

x>5-→

  T, x > 5 is irredundant (Definition 8), thus this transition must be matched by P, true . Hence we can take P, true x>5 -→ T, x > 5 and then T, x > 5 R T, x > 5 . The other pairs are trivially verified. Notice that

  is a partition of IS ⋆ where γ and γ ′ are in B i iff they satisfy the same barbs (↓ c ), Iteration P n+1 := IR (P n ) as in Definition 11 Termination If P n = P n+1 then return P n .

  P, c ⊔ a P ′ , c ′ then there exist α, b ∈ Con 0 s.t. P, c α P ′ , c ′′ where α ⊔ b = a and c ′′ ⊔ b = c ′ .

  hold. Let P = ask α → (ask β → stop) and d = α ⊔ β. Now consider the transition P, d =⇒ stop, d and let us apply the completeness lemma, we can take c = true and a = α ⊔ β, therefore by completeness there must exist b and λ s.t. P, true λ =⇒ stop, c ′′ where λ ⊔ b = α ⊔ β and c ′′ ⊔ b = d.

Definition 19 .

 19 The functions C and L are defined as follows, C([γ, α]) = {γ} and L([γ, α]) = {α}. They extend to set of pairs as expected, namely given a set of pairs S = {p 1 , . . . } then L(S) = p i ∈S L(p i ) and similarly for C.

  Saturated LTS (infinitely branching).

Figure 6 :

 6 Figure 6: CCS Process P = a.P of Example 12

  β⊔λ =⇒ P ′ , c ′ then P, c β =⇒ P ′′ , c ′′ λ =⇒ P ′ , c ′ where β ⊔ λ = α. By induction hypothesis, P, c ⊔ β =⇒ P ′′ , c ′′ (1) and P ′′ , c ′′ ⊔ λ =⇒ P ′ , c ′ (2). By monotonicity on (1), P, c ⊔ β ⊔ λ =⇒ P ′′ , c ′′ ⊔ λ and by rule R-Add on this transition and (2) then, given that β ⊔ λ = α, we obtain P, c ⊔ α =⇒ P ′ , c ′ . Lemma 7 (Completeness of =⇒). If P, c ⊔ a =⇒ P ′ , c ′ then there exist α and b s.t. P, c α =⇒ P ′ , c ′′ where α ⊔ b = a and c ′′ ⊔ b = c ′ .

  Induction) Let us assume that P, c ⊔ a -→ i P i , c i -→ P ′ , c ′ then by induction hypothesis there exist β and b ′ s.t. P, c β =⇒ P i , c ′ i (1) where β ⊔ b ′ = a and c ′ i ⊔ b ′ = c i . Now by completeness on the last transition P i , c ′ i ⊔b ′ c i -→ P ′ , c ′ , there exists λ and b ′′ s.t. P i , c ′ i λ -→ P ′ , c ′′ where λ ⊔ b ′′ = b ′ and c ′′ ⊔ b ′′ = c ′ , thus by rule R-Label we have P i , c ′ i λ =⇒ P ′ , c ′′ (2). We can now proceed to apply rule R-Add on (1) and (2) to obtain the transition P, c α =⇒ P ′ , c ′′ where α = β ⊔ λ and finally take b = b ′′ , therefore the conditions hold α ⊔ b = β ⊔ λ ⊔ b ′′ = a and c ′′ ⊔ b = c ′′ ⊔ b ′′ = c ′ .

Lemma 9 .

 9 hence we can use Lemma 2 again to deduce that Q, d ⊔ α =⇒ Q ′ , d ′ . Finally, by completeness of =⇒, there exist β and b s.t. t = Q, d β =⇒ Q ′ , d ′′ where β ⊔ b = α and d ′′ ⊔ b = d ′ , therefore t ⊢ D Q, d α Q ′ , d ′ and P ′ , c ′ R Q ′ , d ′ . If γ ∼=⇒ sym γ ′ then γ ≈sb γ ′ Proof. We need to prove that R = {( P, c ⊔ a , Q, d ⊔ a ) | P, c ∼=⇒ sym Q, d} is a weak saturated bisimulation. First, condition (i) follows form Lemma 3 and (iii) by definition of R. Let us prove condition (ii), assume P, c ⊔ a -→ * P ′ , c ′ then by Lemma 2 P, c ⊔ a =⇒ P ′ , c ′ . Now by completeness of =⇒ there exist α and b s.t. P, c α =⇒ P ′ , c ′′ where α ⊔ b = a and c ′′ ⊔ b = c ′ . Since P, c ∼=⇒ sym Q, d then we know there exists a transitiont = Q, d β =⇒ Q ′ , d ′ s.t. t ⊢ D Q, d α Q ′ , d ′′ and (a) P ′ , c ′′ ∼=⇒ sym Q ′ , d ′′ , by definition of ⊢ D there exists b ′ s.t. β ⊔ b ′ = α and d ′ ⊔ b ′ = d ′′ . Using soundness of =⇒ on t we get Q, d ⊔ β =⇒ Q ′ , d ′ , thus by Lemma 2 Q, d ⊔ β -→ * Q ′ , d ′ and finally by monotonicity Q, d ⊔ a β ⊔ b ′ α ⊔b -→ * Q ′ , d ′′ d ′ ⊔ b ′ ⊔b (2)Then, the transition P, c ⊔ a -→ * P ′ , c ′ can be rewritten as P, c ⊔ a -→ * P ′ , c ′′ ⊔ b , and using (2), Q, d ⊔ a -→ * Q ′ , d ′′ ⊔ b . It is left to prove that P ′ , c ′′ ⊔ b R Q ′ , d ′′ ⊔ b which follows from (a) and Theorem 1.

Proposition 3 .

 3 Assume that -→ is finitely branching (Definition 18). LetG = LTS -→ (IS ) and G ′ = LTS =⇒ (IS ). Let N = |V(G)| = |E(G)|, N ′ = |V(G ′ )| and M ′ = |E(G)|. We have that N ′ = N and M ′ = O(N 2 ).

Algorithm 3

 3 weak-pr-ccp(IS , ) Initialization 1. Compute IS ⋆ with the rules (IS IS ), (RS IS ), (RD IS ) defined in Table4,2. P 0 = {B 1 } . . . {B m }is a partition of IS ⋆ where γ and γ ′ are in B i iff they satisfy the same weak barbs (⇓ c ), Iteration P n+1 := IR (P n ) as in Definition 11 Termination If P n = P n+1 then return P n . We now show that the size of IS ⋆ =⇒ may be exponential w.r.t. |Config -→ (IS )|. Lemma 10. There exists IS such that |IS ⋆ =⇒ | = Ω(2 |Config -→ (IS )| ).

Figure 8 :

 8 Figure 8: Nodes is the size of Config -→ (IS ) for a given set of initial configurations IS . In (a) we tested the case in which LTS =⇒ (IS ) grows quadratically w.r.t. Nodes by constructing IS as in the worst-case scenario described in Lemma 10. In (b) we generated IS where the size of LTS =⇒ (IS ) grows linearly w.r.t. Nodes.

Table 1 :

 1 Milner's Saturation Method

	MR1	P P	a -→ P ′ a =⇒ P ′		MR2 P	τ =⇒ P
		MR3	P	τ =⇒ P 1 P	a =⇒ P 2 a =⇒ P ′	τ =⇒ P ′

Table 2 :

 2 Reduction semantics for CCP (symmetric rules for R3 and R4 are omitted).

Table 6

 6

	).Con-

I respectively).

Table 6 :

 6 New saturation method.

Table 6

 6 must be replaced by those in Table7(essentially, the lub operation ⊔ of CCP is replaced by the concatenation of sequence).

	RCCS1 P	τ =⇒ CCS P	RCCS2	P P	s -→ CCS P ′ s =⇒ CCS P ′
	RCCS3	P	s =⇒ CCS P ′ s ′ =⇒ CCS P ′′ P s.s ′ =⇒ CCS P ′′

Table 7 :

 7 New Labeled Transition System for CCS. Let s = a 1 . . . a n be a sequence of observable actions. For the Rule RCCS3 we assume that s.τ = τ.s = s.

Notice that we also defined fv (.) on constraints in the previous section.

Notice that in the syntax we have ∃ x P which refers to ∃ e x P when e = true, namely a local process always starts with an empty local store.

Notice that when IS ⋆ denotes the set of reachable configurations then Config (IS ) = IS ⋆ .

Recall that for a given transition t = (s, a, r) the source, the target and the label are src(t) = s, tar (t) = r and lab(t) = a respectively.

Notice that Lemma 2 also holds for the Milner's saturation method (Table5)

Notice that Lemma 3 also holds for the Milner's saturation method (Table5) because of Lemma 2

Acknowledgments. We would like to thank the anonymous reviewers of this paper. Their constructive criticism and suggestions helped us improve the previous versions of this paper.

✩ This work has been partially supported by the projects ANR-09-BLAN-0345 CPP, ANR 12IS02001 PACE and ANR-09-BLAN-0169-01 PANDA; and by the French Defense procurement agency (DGA) with a PhD grant.

Now, under the assumption that -→ is finitely branching, we can observe that if the number of configurations that can be reached (in one or more steps) is finite, then the number of labels should also be finite. Proof. From the hypothesis we know that there are finite γ ′ that can be reached, and using the assumption of being finitely branching we can see that from each of those γ ′ there are only finitely possible α, hence the conclusion.

Finally, the nature of the labels in CCP is one of the reasons why our new transition system works. The following lemma illustrates the fact that when generating new labels, with the rule R-Add (Table 6) we will not add an infinite number of those. In the following, C * ⊔ will represent the Kleene closure over ⊔ of the set of constraints C.

Proof. Follows from the commutativity and idempotency of ⊔ (c ⊔ c = c).

Using these elements, the finitely branching property of =⇒ follows directly under the assumption that -→ is finitely branching and our restriction to finite processes (see Remark 5).

Lemma 5. If -→ is finitely branching then =⇒ is finitely branching.

Proof. (1) |C(Reach * (γ, -→))| < ∞ for every γ due to our restriction to finite processes and our assumption that -→ is finitely branching. One can verify that

(2) From the hypothesis and from Proposition 2 |L(Reach * (γ, -→))| < ∞.

(3) One can check that L(Reach(γ, =⇒)) ⊆ L(Reach * (γ, -→)) * ⊔ therefore from Lemma 4 and ( 2)

From ( 1) and (3) we can conclude that for any γ, =⇒ is finitely branching.

First, we count P n , true and stop, b 0 , hence the +2 in f (n). Furthermore, the rest of the states are those generated by P n 1 , a 0 and these are exactly f (n -1). Moreover, since a 0 ⊏ b 0 then by rule (RD IS ) a new state P n 1 , b 0 is added to IS ⋆ =⇒ . Note that P n 1 , b 0 produces the same number of states as P n 1 , a 0 since by construction a 0 and b 0 are irrelevant in P n 1 . Therefore we count the states generated by P n 1 , b 0 as another f (n -1). Also note that the same reasoning applies at every level of the process. By solving the recurrence we can conclude that f

) as wanted. We can now state correctness and complexity of weak-pr-ccp(IS , =⇒).

Theorem 4. Assume that -→ is finitely branching (Definition 18). Let γ and γ ′ be two CCP configurations. Let IS = {γ, γ ′ } and let P be the output of weak-pr-ccp(IS , =⇒) in Algorithm 3. Then

• weak-pr-ccp(IS , =⇒) may take exponential time in |Config -→ (IS )|.

Proof. The first point follows from Corollary 1 ( ∼=⇒ sym = ∼=⇒ I ) and Theorem 3 ( ∼=⇒ sym = ≈sb ). For the second point, as for the strong case, the exponential time is due to construction of the set IS ⋆ =⇒ in step 1 of weak-pr-ccp(IS , =⇒), whose size is exponential in |Config -→ (IS )| as shown in Lemma 10).

Implementation. We conclude by showing some experiments performed using our tool. In Figure 8 we present the results obtained after running two sets of experiments.

In Figure 8-(a) we evaluate the performance of our procedure in the worstcase scenario described in Lemma 10, which is exponential in |Config -→ (IS )|. Moreover, because of Proposition 3, we know that the size of LTS =⇒ (IS ) can grow (at most) quadratically w.r.t. |Config -→ (IS )|. Consequently, we can see that for Nodes = 10 the algorithm for weak bisimilarity already takes more than the strong one with Nodes = 40.

In Figure 8-(b) we focused on a set of cases in which LTS =⇒ (IS ) grows linearly w.r.t. |Config -→ (IS )|. The idea is to evaluate the performance of the weak