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

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

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

Efficient Algorithms for Program Equivalence for Confluent Concurrent Constraint Programming ✩

Keywords: Concurrent Constraint Programming, Bisimulation, Partition Refinement, Observational Equivalence

Concurrent Constraint Programming (CCP) is a well-established declarative framework from concurrency theory. Its foundations and principles e.g., semantics, proof systems, axiomatizations, have been thoroughly studied for over the last two decades. In contrast, the development of algorithms and automatic verification procedures for CCP have hitherto been far too little considered. To the best of our knowledge there is only one existing verification algorithm for the standard notion of CCP program (observational) equivalence. In this paper we first show that this verification algorithm has an exponential-time complexity even for programs from a representative sub-language of CCP; the summation-free fragment (CCP\+). We then significantly improve on the complexity of this algorithm by providing two alternative polynomial-time decision procedures for CCP\+ program equivalence. Each of these two procedures has an advantage over the other. One has a better time complexity.

language of CCP to produce significant state space reductions. The relevance of both procedures derives from the importance of CCP\+. This fragment, which has been the subject of many theoretical studies, has strong ties to first-order logic and an elegant denotational semantics, and it can be used to model real-world situations. Its most distinctive feature is that of confluence, a property we exploit to obtain our polynomial procedures. Finally, we also study the congruence issues regarding CCP's program equivalence.

Introduction

Motivation. Concurrent constraint programming (CCP) [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF] is a well-established formalism from concurrency theory that combines the traditional algebraic and operational view of process calculi with a declarative one based upon logic. It was designed to give programmers explicit access to the concept of partial information and, as such, has close ties with logic and constraint programming.

The CCP framework models systems whose agents (processes or programs) interact by concurrently posting (telling) and querying (asking for) partial information in a shared medium (the store). This framework is parametric in a constraint system indicating interdependencies (entailment) between partial information and providing for the specification of data types and other rich structures. The above features have attracted renewed attention as witnessed by the works [START_REF] Palamidessi | On the expressiveness of linearity vs persistence in the asychronous pi-calculus[END_REF][START_REF] Buscemi | Open bisimulation for the concurrent constraint pi-calculus[END_REF][START_REF] Bengtson | Psi-calculi: Mobile processes, nominal data, and logic[END_REF][START_REF] Bartoletti | A calculus of contracting processes[END_REF][START_REF] Knight | Spatial and epistemic modalities in constraint-based process calculi[END_REF] on calculi exhibiting data-types, logic assertions as well as tell and ask operations. A compelling example of the kind of system CCP can model involves users interacting by posting and querying information in a social network [START_REF] Knight | Spatial and epistemic modalities in constraint-based process calculi[END_REF].

Nevertheless, despite the extensive research on the foundations and principles of CCP, the development of tools and algorithms for the automatic verification of CCP programs has hitherto been far too little considered. As we shall argue below, the only existing algorithm for deciding the standard notion of process equivalence was given in [START_REF] Pino | Weak CCP bisimilarity with strong procedures[END_REF] and it has an exponential time (and space) complexity.

The main goal of this paper is to produce efficient decision procedures for program equivalence for a meaningful fragment of CCP. Namely, the summation-free fragment of CCP, henceforth CCP\+. The CCP\+ formalism is perhaps the most representative sublanguage of CCP. It has been the subject of many theoretical studies because of its computational expressivity, strong ties to first-order logic, and elegant denotational semantics based on closure operators [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF]. 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.

Approach. To explain our approach we shall briefly recall some CCP equivalences. The standard notion of observational (program) equivalence, ∼ o , [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF], 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 stores. Other alternative notions of program equivalences for CCP such as saturated barbed bisimilarity ( ∼sb ) and its weak variant ( ≈sb ) were introduced in [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF][START_REF] Hofmann | Bisimulation Techniques and Algorithms for Concurrent Constraint Programming[END_REF], where it is also shown that ≈sb coincides with the standard CCP observational equivalence for CCP\+ programs.

The above-mentioned alternative notions of CCP equivalences are defined in terms of a labeled transition system (LTS) describing the interactive behavior of CCP programs. (Intuitively, a labeled transition γ α -→ γ ′ represents the evolution into the program configuration γ ′ if the information α is added to store of the program configuration γ.) The advantage of using these alternative notions of equivalence instead of using directly the standard notion of observational equivalence for CCP is that there is a substantial amount of work supporting the automatic verification of bisimilarity-based equivalence.

Unfortunately, the standard algorithms for checking bisimilarity (such as [START_REF] Kanellakis | CCS expressions, finite state processes, and three problems of equivalence[END_REF][START_REF] Fernandez | Verifying bisimulations "On the Fly[END_REF][START_REF] Bouali | Symbolic bisimulation minimisation[END_REF][START_REF] Dovier | An efficient algorithm for computing bisimulation equivalence[END_REF]) cannot be reused for ∼sb and ≈sb , since in this particular case of the bisimulation game, when the attacker proposes a transition, the defender does not necessarily have to answer with a transition with the same label. (This is analogous to what happens in the asynchronous π-calculus [START_REF] Amadio | On bisimulations for the asynchronous pi-calculus[END_REF] where an input transition can be matched also by an internal (tau) transition.) Partition Refinement for CCP. By building upon [START_REF] Amadio | On bisimulations for the asynchronous pi-calculus[END_REF], we introduced in [START_REF] Aristizábal | Partition refinement for bisimilarity in CCP[END_REF] a variation of the partition refinement algorithm that allows us to decide ∼sb in CCP. The variation 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. Now, if we consider the transition system having only non-redundant transitions, the ordinary notion of bisimilarity coincides with ∼sb . Thus, 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 ?

The solution in [START_REF] Aristizábal | Partition refinement for bisimilarity in CCP[END_REF] consists in computing ∼sb and redundancy at the same time. In the first step, the algorithm considers all the states as equivalent and all the (potentially redundant) transitions as redundant. In any iteration, states are discerned 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 [START_REF] Aristizábal | Partition refinement for bisimilarity in CCP[END_REF] is that in the initial partition, we insert not only the reachable states, but also extra ones which are needed to check for redundancy. Unfortunately, the number of these states might be exponentially bigger than the size of the original LTS and therefore worst-case complexity is exponential, even as we shall show in this paper, for the restricted case of CCP\+.

This becomes even more problematic when considering the weak semantics ≈sb . Usually weak bisimilarity is computed by first closing the transition relation with respect to internal transitions and then by checking strong bisimilarity on the obtained LTS. In [START_REF] Pino | Weak CCP bisimilarity with strong procedures[END_REF], this approach (which is referred in [START_REF] Aceto | The algorithmics of bisimilarity[END_REF] as saturation) is proven to be unsound for CCP (see [START_REF] Pino | Weak CCP bisimilarity with strong procedures[END_REF]). It is also shown that in order to obtain a sound algorithm, one has to close the transition relation, not only w.r.t. the internal transitions, but w.r.t. all the transitions. This induces an explosion of the number of transitions which makes the computation of ≈sb even more inefficient.

Confluent CCP. In this paper, we shall consider the "summation free" fragment of CCP (CCP\+), i.e., the fragment of CCP without non-deterministic choice. Differently from similar fragments of other process calculi (such as the π-calculus or the mobile ambients), CCP\+ is confluent because concurrent constraints programs interact only via reading and telling permanent pieces of information (roughly speaking, resources are not consumed). When considering the weak equivalence ≈sb , confluence makes it possible to characterize redundant transitions syntactically, i.e., without any information about ≈sb . Therefore for checking ≈sb in CCP\+, we can first prune redundant transitions and then check the standard bisimilarity with one of the usual algorithms [START_REF] Kanellakis | CCS expressions, finite state processes, and three problems of equivalence[END_REF][START_REF] Fernandez | Verifying bisimulations "On the Fly[END_REF][START_REF] Bouali | Symbolic bisimulation minimisation[END_REF][START_REF] Dovier | An efficient algorithm for computing bisimulation equivalence[END_REF]. Since redundancy can be determined statically, the additional states needed by the algorithm in [START_REF] Aristizábal | Partition refinement for bisimilarity in CCP[END_REF] are not necessary any more: in this way, the worst case complexity from exponential becomes polynomial.

Unfortunately, this approach still suffers of the explosion of transitions caused by the closure of the transition relation. In order to avoid this problem, we exploit a completely different approach (based on the semantic notion of compact inputoutput sets) that works directly on the original LTS. We shall conclude our paper by also showing how the results obtained for CCP\+can be exploited to optimize the partition refinement for the full language of CCP.

We wish to conclude this introduction with a quote from [START_REF] Garavel | Reflections on the future of concurrency theory in general and process calculi in particular[END_REF] that captures the goal of the present paper: "The times have gone, where formal methods were primarily a pen-and-pencil activity for mathematicians. Today, only languages properly equipped with software tools will have a chance to be adopted by industry. It is therefore essential for the next generation of languages based on process calculi to be supported by compilers, simulators, verification tools, etc. The research agenda for theoretical concurrency should therefore address the design of efficient algorithms for translating and verifying formal specifications of concurrent systems".

Contributions. This paper is an extended version of [START_REF] Pino | Efficient computation of program equivalence for confluent concurrent constraint programming[END_REF]. In this version we give all the details and proofs omitted in [START_REF] Pino | Efficient computation of program equivalence for confluent concurrent constraint programming[END_REF]. We also extend the intuitions from [START_REF] Pino | Efficient computation of program equivalence for confluent concurrent constraint programming[END_REF] to improve the clarity of the paper. Furthermore, we add a section, Section 7, with new technical material. In this new section we study congruence issues for the CCP fragment here studied, CCP\+, as well as for the full language of CCP. In particular we show that ≈sb is a congruence for CCP\+ but not for CCP. Despite the negative result for the full language we show that ≈sb is still a useful notion as it implies the standard notion of program equivalence ∼ o for CCP. Consequently, the (co-inductive) proof techniques associated to ≈sb can be used to establish program equivalence and the algorithms provided in this paper for the full language can be used as semi-decision procedures for ∼ o .

Structure of the paper. The paper is organized as follows: In Section 2 we recall the background concerning the standard partition refinement and the CCP formalism. In Section 3 we present the partition refinement for CCP from [START_REF] Aristizábal | Partition refinement for bisimilarity in CCP[END_REF] and how it can be used to decide observational equivalence following [START_REF] Pino | Weak CCP bisimilarity with strong procedures[END_REF]. Our contributions begin in Section 4 where we prove that the partition refinement for CCP from Section 3 is inefficient even for CCP\+. We then introduce some particular features of CCP\+ which are then used to develop a polynomial procedure for checking observational equivalence in CCP\+. In Section 5 we introduce our second, more efficient, method for deciding observational equivalence by using the compact input-output sets. In Section 6 we show how the procedure from Section 4 can be adapted to the full CCP language. In Section 7 we discuss the use of the technique in Section 6 as a semi-decision procedure for observational equivalence. We also discuss the congruence issues concerning weak bisimilarity for CCP and CCP\+. Finally, in Section 8 we present our conclusions and future work.

Background

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, the concurrent constraint programming (CCP) and we show that partition refinement cannot be used for checking equivalence of concurrent constraint processes.

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.

Partition Refinement

We report 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 1See 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 .

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 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. (Constraint System) A constraint system (cs) is a complete algebraic lattice C = (Con, Con 0 , ⊑, ⊔, true, false) where Con, the set of constraints, is a partially ordered set w.r.t. ⊑, 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. Remark 1. We assume that the constraint system is well-founded and that its ordering ⊑ is decidable.

We now define the constraint system we use in our examples.

Example 1. Let Var be a set of variables and ω be the set of natural numbers. A variable assignment is a function µ : Var -→ ω. We use A to denote the set of all assignments, P(A) to denote the powerset of A, ∅ the empty set and ∩ the intersection of sets. Let us define the following constraint system: The set of constraints is P(A). We 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. We will often use a formula like x < n to denote the corresponding constraint, i.e., the set of all assignments that map x to a number smaller than n.

Syntax

We now recall the basic CCP process constructions. We are concerned with the verification of finite-state systems, thus we shall dispense with the recursion operator which is meant for describing infinite behavior. We shall also omit the local/hiding operator for the simplicity of the presentation (see [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF][START_REF] Hofmann | Bisimulation Techniques and Algorithms for Concurrent Constraint Programming[END_REF] for further details).

Let C = (Con, Con 0 , ⊑, ⊔, true, false) a constraint system. The CCP processes are given by the following syntax:

P, Q ::= stop | tell(c) | ask(c) → P | P Q | P + Q
where c ∈ Con 0 . Intuitively, stop represents termination, tell(c) adds the constraint (or partial information) c to the store. The addition is performed regardless the generation of inconsistent information. The process ask(c) → P may execute P if c is entailed from 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.

Remark 2. (CCP\+)

. Henceforth, we use CCP\+ to refer to the fragment of CCP without nondeterministic choice.

Reduction Semantics

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 all configurations. We will use Conf CCP\+ for the CCP\+ configurations. The operational semantics of CCP is given by an unlabeled transition relation between 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 -→.

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 ′
Formally, the reduction semantics of CCP is given by the relation -→ defined in Table 1. These rules are easily seen to realize the intuitions described in the syntax (Section 2.3).

In [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF][START_REF] Hofmann | Bisimulation Techniques and Algorithms for Concurrent Constraint Programming[END_REF], the authors introduced a barbed semantics for CCP. Barbed equivalences have been introduced in [START_REF] Milner | Barbed bisimulation[END_REF] for CCS, and have become a classical way to define the semantics of 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, written γ ↓ c , iff c ⊑ d. Similarly, γ satisfies a weak barb c, written γ ⇓ c , iff there exist

γ ′ s.t. γ -→ * γ ′ ↓ c . Example 2. Let γ = ask (x > 10) → tell(y < 42), x > 10 . We have γ ↓ x>5 since (x > 5) ⊑ (x > 10) and γ ⇓ y<42 since γ -→ tell(y < 42), x > 10 -→ stop, (x > 10) ⊔ (y < 42) ↓ y<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 is a saturated barbed bisimulation R s.t. (γ 1 , γ 2 ) ∈ R. We write P ∼sb Q iff P, true ∼sb Q, true .
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 (-→ * ).

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. We write P ≈sb Q iff P, true ≈sb Q, true .

We now illustrate ∼sb and ≈sb with the following two examples.

Example 3. Take T = tell(true), P = ask (x < 7) → T and Q = ask (x < 5) → T . One can check that P, true ∼sb Q, true , since P, x < 7 -→ T, x < 7 , while Q, x < 7 -→. Then consider P + Q, true and observe that P + Q, true ∼sb P, true . Indeed, for all constraints e, s.t. x < 7 ⊑ e, both the configurations evolve into T, e , while for all e s.t. x < 7 ⊑ e, both configurations cannot proceed. Since x < 7 ⊑ x < 5, the behavior of Q is in a sense absorbed by the behavior of P .

R = {(γ 2 , γ 1 ), (γ 2 , stop, true ), ( tell(d), c , stop, c ), ( stop, c , stop, c )}
is a weak saturated barbed bisimulation as in Definition 4.

Labeled Semantics

In [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF][START_REF] Hofmann | Bisimulation Techniques and Algorithms for Concurrent Constraint Programming[END_REF] we have shown that ≈sb is fully abstract with respect to the standard observational equivalence from [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF]. Unfortunately, the quantification over all constraints in condition (iii) of Definition 3 and Definition 4 makes checking ∼sb and ≈sb hard, since one should check infinitely many constraints. In order to avoid this problem we have introduced in [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF][START_REF] Hofmann | Bisimulation Techniques and Algorithms for Concurrent Constraint Programming[END_REF] a labeled transition semantics where labels are constraints.

In a transition of the form P, d α -→ P ′ , d ′ the label α ∈ Con 0 represents a minimal information (from the environment) that needs to be added to the store d to reduce from P, d to P ′ , d ′ , i.e., P, d ⊔ α -→ P ′ , d ′ . This approach is based on [START_REF] Bonchi | Symbolic semantics revisited[END_REF] which is related to the early work on symbolic semantics from [START_REF] Hennessy | Symbolic bisimulations[END_REF].

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 means true . Given a set of

initial configurations IS , Config (IS ) denotes the set {γ ′ | ∃γ ∈ IS s.t. γ α 1 . . . αn γ ′ for some n ≥ 0}.
The LTS (Conf , Con 0 , -→) is defined by the rules in Table 2. 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}. The other rules are easily seen to realize the intuition given in Section 2.3. Figure 2 illustrates the LTS of our running example.

Given the LTS (Conf , Con 0 , -→), one would like to exploit it for "efficiently characterizing" ∼sb and ≈sb . One first naive attempt would be to consider the standard notion of (weak) bisimilarity over -→, but this would distinguish configurations which are in ∼sb (and ≈sb ), as illustrated by the following two examples.

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 ′
Table 2: Labeled semantics for CCP (the symmetric rules for LR3 and LR4 are omitted).

T = tell(true) T ′ = tell(y = 1) P = ask (x < 7) → T S = ask (z < 7) → P Q = ask (x < 5) → T Q ′ = ask (x < 5) → T ′ R = ask (z < 5) → (P + Q) R ′ = ask (z < 5) → (P + Q ′ ) R + S, true S, true R ′ + S, true P + Q ′ , z < 5 P, z < 7 P + Q, z < 5 P, z < 5 T ′ , z < 5 ⊔ x < 5 T, z < 7 ⊔ x < 7 T, z < 5 ⊔ x < 5 T, z < 5 ⊔ x < 7 stop, z < 5 ⊔ x < 5 ⊔ y = 1 stop, z < 7 ⊔ x < 7 stop, z < 5 ⊔ x < 5 stop, z < 5 ⊔ x < 7 x < 7 z < 5 z < 7 z < 7 z < 5 z < 7
x < 5

x < 7

x < 5

x < 7 The examples above show that the ordinary notion of bisimilarity do not coincide with the intended semantics ( ∼sb and ≈sb ). As a consequence, the standard partition refinement algorithm (Section 2.1) cannot be used for checking ∼sb and ≈sb . However, one can consider a variation of the bisimulation game, namely irredundant bisimilarity [START_REF] Aristizábal | Partition refinement for bisimilarity in CCP[END_REF], which coincide with ∼sb and, in the weak case [START_REF] Pino | Weak CCP bisimilarity with strong procedures[END_REF], with ≈sb . This fact allowed us in [START_REF] Aristizábal | Partition refinement for bisimilarity in CCP[END_REF] to define a variation of the partition refinement algorithm which we show in the next section.

First, we recall some results from [START_REF] Aristizábal | Partition refinement for bisimilarity in CCP[END_REF] and [START_REF] Pino | Weak CCP bisimilarity with strong procedures[END_REF], which are fundamental for the development of the paper.

R-Tau γ =⇒ γ R-Label γ α -→ γ ′ γ α =⇒ γ ′ R-Add γ α =⇒ γ ′ β =⇒ γ ′′ γ α⊔β =⇒ γ ′′ Table 3: Weak semantics for CCP Lemma 1. ([8, 9], [7]) (Soundness) If P, c α -→ P ′ , c ′ then P, c ⊔ α -→ P ′ , c ′ . (Completeness) If P, c ⊔ a -→ P ′ , c ′ then there exists α and b s.t. P, c α -→ P ′ , c ′′ where α ⊔ b = a and c ′′ ⊔ b = c ′ .
The weak labeled transition system (Conf , Con 0 , =⇒) is defined by the rules in Table 3. This LTS is sound and complete, as -→, and it can be used to decide ≈sb as shown in [START_REF] Pino | Weak CCP bisimilarity with strong procedures[END_REF].

Lemma 2. ([7]) (Soundness) If P, c α =⇒ P ′ , c ′ then P, c ⊔ α =⇒ P ′ , c ′ . (Completeness) If P, c ⊔ a =⇒ P ′ , c ′ then there exists α and b s.t. P, c α =⇒ P ′ , c ′′ where α ⊔ b = a and c ′′ ⊔ b = c ′ .
Note that we close -→, not only w.r.t true transitions (as similarly done in CCS, where τ intuitively corresponds to true), but w.r.t. all the transitions. This is needed to check ≈sb , because otherwise the above lemma would not hold.

Finally, the following lemma relates the labeled and weak semantics, i.e. -→ and =⇒. It states that a single transition in =⇒ corresponds to a sequence of reductions (-→ * ).

Lemma 3. ([7]) γ -→ * γ ′ iff γ =⇒ γ ′ .

Partition refinement for CCP

In this section we recall the partition refinement algorithm for CCP and how it can be used to decide observational equivalence.

Strong equivalence

In [START_REF] Aristizábal | Partition refinement for bisimilarity in CCP[END_REF], we adapted the standard partition refinement procedure to check strong bisimilarity for CCP ( ∼sb ) by relying on [START_REF] Bonchi | Minimization algorithm for symbolic bisimilarity[END_REF] (which, in turn, was inspired by [START_REF] Pistore | A partition refinement algorithm for the π-calculus[END_REF] presenting a similar procedure for the open π-calculus). As we did for the standard partition refinement, we also 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. Now, since configurations satisfying different barbs are surely different, it can be safely started with a partition that equates all and only those states 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.

When splitting the above-mentioned partitions, 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 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 ≻ t ′ , iff α ⊏ β and c ′′ = c ′ ⊔ β.
The intuition is that the transition t dominates t ′ iff t requires less 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. and let γ = P, true . Now let t 1 and t 2 be transitions defined as:

t 1 = γ x<15 -→ tell(y > 42), x < 15 and t 2 = γ x<10 -→ tell(y > 42), x < 10
One can check that t 1 ≻ t 2 since (x < 15) ⊏ (x < 10) and also (x < 10) = ((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 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 ≻ 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.

To understand this definition better consider the following example.

(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 ⋆
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: We now explain briefly how to compute IS ⋆ using the Rules in Table 4. Rules (IS IS ) and (RS IS ) say that all the states generated from the labeled semantics (Table 2) from the set of initial states should be included, i.e., Config (IS ) ⊆ IS ⋆ .

t = γ a -→ stop, a and t ′ = γ b -→ ask (c) → tell(d), b Finally, let R = ≈sb
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 6 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 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, we shall describe how the refinement is done in the case CCP. Instead of using the function F (P) of Algorithm 1, the partitions are refined by employing the function IR (P) defined as follows.

γ a 1 γ b 1 γ 2 γ a 2 γ 1 , γ a 1 , γ b 1 , γ 2 , γ a 2 γ 1 , γ 2 γ a 1 , γ b 1 , γ a 2 P IR -→ (P)
γ 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
See Figure 3 for an example of the use of IR (-).

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 strong saturated bisimilarity ∼sb with exponential time. (Recall that Config -→ (IS ) represents the set of states that are reachable from the initial states IS using -→.) More precisely: Theorem 1. ( [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. 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 )|.

Weak equivalence

We can also use the above-mentioned algorithm to verify the weak version of saturated barbed bisimilarity ( ≈sb ). Recall that, as shown in [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF][START_REF] Hofmann | Bisimulation Techniques and Algorithms for Concurrent Constraint Programming[END_REF], in CCP\+ weak bisimilarity ( ≈sb ) coincides with the standard notion of CCP program (observational) equivalence.

Following [START_REF] Aceto | The algorithmics of bisimilarity[END_REF] the reduction of the problem of deciding ≈sb to the problem of deciding ∼sb is obtained by adding some additional transitions, so called weak transitions, to the LTS. Given two configurations γ and γ ′ , the first step is to build G = LTS -→ (IS ) where IS = {γ, γ ′ }. Using G we then proceed to compute G ′ = LTS =⇒ (IS ), and finally we run Algorithm 2 adapted to G ′ . The adaptation consists in using weak barbs (⇓ c ) instead of barbs (↓ c ) for the initial partition P 0 and using =⇒ as a parameter of the algorithm. Using Algorithm 3 we can decide ≈sb also with exponential time.

Theorem 2. ( [START_REF] Pino | Weak CCP bisimilarity with strong procedures[END_REF]) Let γ and γ ′ be two CCP configurations. Let IS = {γ, γ ′ } and let P be the output of weak-pr-ccp(IS , =⇒) defined in Algorithm 3. Then

• γ P γ ′ iff γ ≈sb γ ′ .
• weak-pr-ccp(IS , =⇒) may take exponential time in |Config -→ (IS )|.

As for the strong case, the exponential time is due to construction of the set IS ⋆ =⇒ by weak-pr-ccp(IS , =⇒), whose size is exponential in |Config -→ (IS )|. In the next section we shall address the issue of avoiding this exponential construction in the context of confluent CCP.

Using Partition refinement for checking observational equivalence in CCP\+

In the previous section, we presented a procedure to verify ≈sb for CCP and we saw how this method takes exponential time (in the size of the LTS) to check whether two configurations are weakly bisimilar. In this section, we will explore what happens with such procedure when we restrict ourselves to CCP\+. We shall see that pr-ccp(IS , -→) may also be exponential time for inputs from the CCP\+ fragment.

Let us consider the following CCP\+ construction.

Example 9. 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 (a i ) → (ask (b i ) → P n i+1 )) (ask (b i ) → stop)
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 LTS for P n , true is illustrated in Figure 4.

One can verify that by taking IS = { P n , true } as in the example above, then the size of IS ⋆ -→ in Algorithm 2 grows exponentially with n, essentially because of the rule (RD IS -→ ).

Proposition 1. Let γ = P n , true as in Example 9 and take IS = {γ}. Let P be the output of pr-ccp(IS , -→) using Algorithm 2, then pr-ccp(IS , -→) takes at least exponential time in n.

The main problem is that the procedure does not distinguish between summationfree processes and the normal CCP processes. Therefore, it is unable to exploit the underlying properties of CCP\+ and the algorithm will perform (in the worstcase) inherently the same as for the full CCP, as evidenced in the example above.

Properties of CCP\+

In this section we will state some features that (unlike the full CCP) this fragment possess. The first one we want to introduce is confluence. Intuitively, in CCP\+, if from a given configuration we have two possible reductions (-→), then we are guaranteed that they will coincide at some point of the computation. Recall that Conf CCP\+ is the set of all CCP\+ configurations, i.e. configurations whose process is summation-free. Before discussing the second property, we need to introduce some notation. We shall call derivatives (of γ) the successors reached via (zero or more) reductions (-→ * ) starting from a given configuration γ.

P n , true LP n 0 , a 0 RP n 0 , b 0 LLP n 0 , b 0 LRP n 0 , b 0 a 0 b 0 b 0 b 0 P n 1 , b 0 P n = (ask (a 0 ) → (ask (b 0 ) → P n 1 )) (ask (b 0 ) → stop) LP n 0 = (ask (b 0 ) → P n 1 ) (ask (b 0 ) → stop) RP n 0 = (ask (a i ) → (ask (b i ) → P n i+1 )) stop) LLP n 0 = P n 1 (ask (b 0 ) → stop) LRP n 0 = (ask (b 0 ) → P n 1 ) stop New nodes after Rule (RD IS -→ ) LP n 0 , b 0 LP n 1 , b 0 ⊔ b 1 LP n 1 , b 0 ⊔ b 1

Definition 8. (Derivatives)

The derivatives of a configuration γ, written Deriv(γ), are defined as

Deriv(γ) = {γ ′ | γ -→ * γ ′ }.
Using this notation, we can now state another property of CCP\+. A CCP\+ configuration is weakly bisimilar to all its derivatives. The proof above relies on the intrinsic confluent nature of CCP\+ (Proposition 2) and this lemma will be central for the results we will present next. In the next section we shall take advantage of these properties to check ≈sb for CCP\+ configurations.

Optimizations to partition refinement for CCP\+

We presented how the partition refinement for CCP performs for CCP\+ as well as some properties of the configurations of this fragment. In this section, using such features, we shall show that the complexity of weak-pr-ccp(IS , =⇒) can be improved, thus we can check ≈sb in a more efficient manner.

Due to the nature of CCP\+, determining which are the redundant transitions w.r.t. ≈sb (Definition 6) becomes an easier task. As we explained in Section 3.1, the purpose of rule (RD IS ) from Table 4 is to add some configurations to IS ⋆ that will be used to check redundancy at each iteration of Algorithm 2. In CCP\+ these additional configurations are not necessary. But before we arrive to this let us introduce some definitions first. Definition 9. We say that γ goes with α to γ ′ with a maximal weak transition, written γ

α =⇒ max γ ′ , iff γ α =⇒ γ ′ -→.
The definition above reflects the fact that when γ α =⇒ max γ ′ then γ ′ has no more information to deduce without the aid of the environment, namely no further reduction (-→) is possible. As =⇒, the maximal weak transition relation =⇒ max is sound and complete. Proof. Follows from the correctness of =⇒ (Lemma 2) and from the fact that LTS -→ ({ P, c }) is finite.

As one would expect, =⇒ max can also be used to compute ≈sb and the complexity of the procedure is equivalent to the case of =⇒ (Theorem 2). Theorem 3. ( [START_REF] Pino | Weak CCP bisimilarity with strong procedures[END_REF]) Let γ and γ ′ be two CCP configurations. Let IS = {γ, γ ′ }, let P be the output weak-pr-ccp(IS , =⇒ max ) using Algorithm 3. Then

• γ P γ ′ iff γ ≈sb γ ′ .
• weak-pr-ccp(IS , =⇒ max ) may take exponential time in |Config -→ (IS )|.

Proof. Follows from the correctness of =⇒ max (Lemma 5); Corollary 1 and Theorem 3 from [START_REF] Pino | Weak CCP bisimilarity with strong procedures[END_REF] and Theorem 2.

Nevertheless, in CCP\+, the maximal weak transitions =⇒ max satisfy a particular property that allow us to erase the redundant transitions w.r.t. ≈sb before computing ≈sb itself.

Proposition 3. Let γ = P, c ∈ Conf CCP\+ . Let t 1 = γ α =⇒ max P 1 , c 1 and t 2 = γ β =⇒ max P 2 , c 2 . We have that α ⊏ β and P 1 , c 1 ⊔ β -→ * P ′ , c 2 -→ iff t 1 ≻ ≈sb t 2 .
Proof. (⇒) By soundness on t 1 we have P, c ⊔ α =⇒ max P 1 , c 1 then by definition P, c ⊔ α =⇒ P 1 , c 1 now by monotonicity P, c ⊔ β =⇒ P 1 , c 1 ⊔ β and then P, c ⊔ β -→ * P 1 , c 1 ⊔ β then by Lemma 4 P, c ⊔ β ≈sb P 1 , c 1 ⊔ β . Using a similar reasoning on t 2 we can conclude that P, c ⊔ β ≈sb P 2 , c 2 and by transitivity P 1 , c 1 ⊔ β ≈sb P 2 , c 2 . Finally take t ′ = (γ, β, P 1 , c 1 ⊔ β ), hence we can conclude that t 1 ≻ ≈sb t 2 since t 1 ≻ t ′ and P 1 , c 1 ⊔ β ≈sb P 2 , c 2 .

(⇐) Assume that t 1 ≻ ≈sb t 2 then there exists t ′ = (γ, β, P 1 , c ′ ) such that t 1 ≻ t ′ and P 1 , c ′ ≈sb P 2 , c 2 . By t 1 ≻ t ′ we know that α ⊏ β and c ′ = c 1 ⊔ β. Now since P 2 , c 2 -→ by definition of =⇒ max , therefore by condition (i) of ≈sb we have c ′ ⊑ c 2 . Moreover, P 1 , c ′ -→ * P ′ , c 3 where c 2 ⊑ c 3 . By contradiction let c 2 = c 3 then c 2 ⊏ c 3 , thus there is e s.t. P 1 , c ′ ⇓ e but since P 2 , c 2 -→ then P 2 , c 2 ⇓ e and so P 1 , c ′ ≈sb P 2 , c 2 , an absurd. Thus

c 3 = c 2 hence P 1 , c ′ -→ * P ′ , c 2 -→ .
Using this property we can define a new procedure for deciding ≈sb that does not use Rule (RD IS ) since redundancy can be checked and erased using Proposition 3 (Algorithm 4, Step 2).

In other words, we first need to build the LTS of reachable states using =⇒ max . Then for each pair of transitions with the same source we can check whether Proposition 3 holds, if it is the case then the redundant transition is removed. Finally we apply the standard partition refinement on the LTS resulting from the previous step. Iteration P n+1 := F =⇒max (P n ) as defined in Equation 1Termination If P n = P n+1 then return P n .

The key idea is that in order to compute ≈sb , with the redundancy removed, it suffices to refine the partitions using F =⇒max (P) (defined by Equation 1) instead of IR =⇒max (P). Algorithm 4 can be used to decide ≈sb for configurations in Conf CCP\+ with polynomial time. Thanks to Proposition 3, by removing redundant transitions, we can solve the problem of checking bisimilarity for CCP\+ with the standard solutions for checking bisimilarity. In Algorithm 4, we have used the "classical" partition refinement, but different, more effective solutions, are possible. For instance, executing the algorithm in [START_REF] Dovier | An efficient algorithm for computing bisimulation equivalence[END_REF] (after having removed all the redundant transitions) would require at most O(|E| + |V |) steps. Note however that, due to the closure needed for weak transitions (Table 3), |E| is usually quadratic w.r.t. the number of states |V |. In the following section, we introduce a novel procedure which avoids such expensive closure.

Using the compact input-output sets for verifying observational equivalence in CCP\+

In the previous section we improved the CCP exponential-time decision procedure for ≈sb to obtain a polynomial-time procedure for the special case of the summation-free fragment CCP\+. (Recall that in CCP\+, the relation ≈sb coincides with the standard notion of observational equivalence.)

In this section, we will present an alternative approach for verifying observational equivalence for CCP\+ that improves on the time and space complexity of Algorithm 4.

Roughly speaking our approach consists in reducing the problem of whether two given CCP\+ configurations γ, γ ′ are in ≈sb to the problem of whether γ and γ ′ have the same minimal finite representation of the set of weak barbs they satisfy in every possible context.

Weak bisimilarity and barb equivalence

First we will show that, in CCP\+, we can give characterization of ≈sb in terms of the simpler notion of weak-barb equivalence defined below. Intuitively, two configurations are saturated weakly bisimilar if and only if for every possible augmentation of their stores, the resulting configurations satisfy the same weak barbs. More precisely, Intuitively, each pair (α, e) ∈ P, c denotes a stimulus-response, or inputoutput, interaction of γ = P, c : If the environment adds α to the store of γ, the resulting configuration P, c ⊔ α may evolve, without any further interaction with the environment, into a configuration whose store entails e. In other words P, c ⊔ α ⇓ e . We can think of e as piece of information that P, c ⊔ α may produce.

The following corollary is an immediate consequence of the definitions. We now introduce the notion of relevant input-output pair.

Definition 12. (Relevant Pair) Let (α, e) and (β, e ′ ) be elements from Con 0 × Con 0 . We say that (α, e) is more relevant than (β, e ′ ), written (α, e) (β, e ′ ), iff α ⊑ β and e ′ ⊑ (e ⊔ β). Similarly, given p = (β, e ′ ) s.t. p ∈ S, we say that the pair p is irrelevant in S if there is a pair (α, e) ∈ S more relevant than p, else p is said to be relevant in S.

Let us illustrate this with an example.

Example 12. Let S = {(true, true), (α, α), (α ⊔ β, α ⊔ β ⊔ c)} where α, β, c ∈ Con 0 are not related to each other. Notice that (true, true) (α, α) however (true, true) (α⊔β, α⊔β⊔c). This means that (true, true) and (α⊔β, α⊔β⊔c) are relevant in S and (α, α) is irrelevant in S.

Recall the stimulus-response intuition given above. In other words, the pair (β, e ′ ) is irrelevant in a given input-output set if there exists another pair (α, e) in the set that represents the need for less stimulus from the environment, hence the condition α ⊑ β, to produce at least as much information, with the possible exception of information that β may entail but α does not. Hence e ′ ⊑ e ⊔ β.

We now list two important properties of that will be useful later on. The set P, c is closed w.r.t. .

A canonical representation of CCP\+ configurations

Clearly P, c may be infinite due potential existence of infinitely many arbitrary stimuli (inputs). By using the labeled transition semantics (Table 2) we shall show that we do not need consider arbitrary inputs but only the minimal ones. Recall that in γ α -→ γ ′ the label α represents the minimal information needed to evolve from γ to γ ′ . Definition 13. The label-based input-output set of a configuration P, c , denoted as M( P, c ), is inductively defined as follows:

{(true, c)} ∪ P,c α -→ P ′ ,c ′ ({(α, c ′ )} ∪ (α ⊗ M( P ′ , c ′ )))
where ⊗ : Con 0 × 2 Con 0 ×Con 0 -→ 2 Con 0 ×Con 0 is defined as

α ⊗ S def = {(α ⊔ β, e) | (β, e) ∈ S)}
Let us illustrate this definition with an example.

Example 13. Let γ = ask (α) → (ask (β) → tell(c)), true and γ ′ = ask (α ⊔ β) → tell(c), true where α, β, c ∈ Con 0 are not related to each other. Let us assume that α and β are the minimal elements that allow γ and γ ′ to proceed. Their corresponding label-based input-output sets are as follows:

M(γ) = {(true, true), (α, α), (α ⊔ β, α ⊔ β), (α ⊔ β, α ⊔ β ⊔ c)} M(γ ′ ) = {(true, true), (α ⊔ β, α ⊔ β), (α ⊔ β, α ⊔ β ⊔ c)}
Nevertheless, labeled-based input-output sets do not give us a fully-abstract representation of the input-output sets because of the existence of irrelevant pairs. By excluding these pairs we obtain a compact and fully-abstract representation of input-output sets.

M C (γ) = M C (γ ′ ) = {(true, true), (α ⊔ β, α ⊔ β ⊔ c)}
We shall now show the full-abstraction of the compact input-output sets. We need the following lemmata. First, compact sets are closed under weak transitions (=⇒). More precisely:

Proposition 6. If P, c α =⇒ P ′ , c ′ then (α, c ′ ) ∈ M( P, c ).
Proof. By induction on the depth of the inference of P, c α =⇒ P ′ , c ′ . Consider the rules R-Tau, R-Label and R-Add from Table 5.

• Using Rule R-Tau we have P, c =⇒ P, c and (true, c) ∈ M( P, c ) by definition.

• Using Rule R-Label we have P, c α -→ P ′ , c ′ and (α, c ′ ) ∈ M( P, c ) by definition.

• Using Rule R-Add we have P, c

α ′′ =⇒ P ′′ , c ′′ α ′ =⇒ P ′ , c ′ where α ′ ⊔ α ′′ = α. Then by induction hypothesis (α ′′ , c ′′ ) ∈ M( P, c ) and (α ′ , c ′ ) ∈ M( P ′′ , c ′′ ), hence by definition of M( P, c ) we have (α ′ ⊔ α ′′ , c ′ ) ∈ M( P, c ) so (α, c ′ ) ∈ M( P, c ).
The following proposition states that whenever a pair (α, e) is in M( P, c ), it means that e can be reached from P, c ⊔ α without aid of the environment. We can now prove our main result, given two configurations P, c and Q, d , they are observationally equivalent if and only if their compact input-output sets are identical. We split the proof in the following two lemmata.

Lemma 6. If M C ( P, c ) = M C ( Q, d ) then P, c = Q, d
Proof. Let us assume that (α, β) ∈ P, c then by definition P, c ⊔ α ⇓ β hence there exists P ′ and β ′ such that P, c ⊔ α -→ * P ′ , β ′ and β ⊑ β ′ . By Lemma 3 we have P, c ⊔ α =⇒ P ′ , β ′ , then by completeness of =⇒ (Lemma 2) there

exist α ′ , b s.t. P, c α ′ =⇒ P ′ , c ′ where α ′ ⊔ b = α and c ′ ⊔ b = β ′ (1). Now by Proposition 6 we know (α ′ , c ′ ) ∈ M( P, c ), then since is well-founded (Proposition 5) there is (α ′′ , c ′′ ) that is relevant in M( P, c ) (then it belongs to M C ( P, c )) such that (α ′′ , c ′′ ) (α ′ , c ′ ), namely α ′′ ⊑ α ′ (or equivalently ∃x.(α ′′ ⊔ x) = α ′ (2)) and c ′ ⊑ (c ′′ ⊔ α ′ ). Given that (α ′′ , c ′′ ) ∈ M C ( P, c ) then by hypothesis (α ′′ , c ′′ ) ∈ M C ( Q, d ), this means also that (α ′′ , c ′′ ) ∈ M( Q, d ) and by Proposition 7 we know that Q, d ⊔ α ′′ -→ * Q ′ , c ′′ . By monotonicity we have the following transition Q, d ⊔ α ′′ ⊔ x ⊔ b -→ * Q ′ , c ′′ ⊔ x ⊔ b , now notice that from (1) and (2) we have (d ⊔ α ′′ ⊔ x ⊔ b) = (d ⊔ α ′ ⊔ b) = (d ⊔ α) then Q, d ⊔ α -→ * Q ′ , c ′′ ⊔ x ⊔ b . Finally, we have to prove that β ⊑ (c ′′ ⊔ x ⊔ b) to conclude that (α, β) ∈ Q, d , for that purpose, recall that β ⊑ β ′ = (c ′ ⊔ b) ⊑ (c ′′ ⊔ α ′ ⊔ b) and since (c ′′ ⊔ α ′′ ⊔ x ⊔ b) = (c ′′ ⊔ x ⊔ b) then β ⊑ (c ′′ ⊔ x ⊔ b) and so (α, β) ∈ Q, d . Lemma 7. If P, c = Q, d then M C ( P, c ) = M C ( Q, d ) Proof. Assume that (α, β) ∈ M C ( P, c ) our goal is to prove that (α, β) ∈ M C ( Q, d ).
By definition (α, β) is relevant in M( P, c ), moreover, by Proposition 7 we have P, c ⊔ α -→ * P ′ , β then by definition (α, β) ∈ P, c and by hypothesis (α,

β) ∈ Q, d . This means that Q, d ⊔ α ⇓ β then there exists Q ′ , d ′ s.t. Q, d ⊔ α -→ * Q ′ , d ′ where β ⊑ d ′ . By Lemma 3 we have Q, d ⊔ α =⇒ Q ′ , d ′ , now by completeness of =⇒ (Lemma 2) there exist α ′ , b s.t. Q, d α ′ =⇒ Q ′ , d ′′ where (α ′ ⊔ b) = α and (d ′′ ⊔ b) = d ′ . Now let us as- sume by means of contradiction that α ′ = α. By soundness of =⇒ (Lemma 2) we have Q, d ⊔ α ′ =⇒ Q ′ , d ′′ then by Lemma 3 we get Q, d ⊔ α ′ -→ * Q ′ , d ′′ hence (α ′ , d ′′ ) ∈ Q, d
. By hypothesis then (α ′ , d ′′ ) ∈ P, c , now this means that P, c ⊔ α ′ -→ * P ′′ , e where d ′′ ⊑ e (equivalently ∃z.(d ′′ ⊔ z) = e). By Lemma 3 we get that P, c ⊔ α ′ =⇒ P ′′ , e and by completeness there exist x, b ′ s.t. P, c

x =⇒ P ′′ , c ′ where (x ⊔ b ′ ) = α ′ and c ′ ⊔ b ′ = e. Using Lemma 6 we have that (x, c ′ ) ∈ M( P, c ), now we will prove that (x, c ′ ) (α, β), ). The first condition follows from y ⊔ b ′′ = α and for the latter condition we proceed as follows 2 ). First a ⊑ α 1 ⊑ α, for the latter condition we proceed as follows

namely x ⊑ α and β ⊑ (α ⊔ c ′ ). Recall that x ⊑ α ′ ⊑ α, now for the latter condition (α ⊔ c ′ ) = (α ′ ⊔ b ⊔ c ′ ) = (x ⊔ b ′ ⊔ b ⊔ c ′ ) = (x ⊔ b ⊔ e) then since d ′′ ⊑ e we can check that β ⊑ d ′ ⊑ (d ′ ⊔ x) = (d ′′ ⊔ b ⊔ x) ⊑ (e ⊔ b ⊔ x) = (α ⊔ c ′ ).
β ⊏ d ′ ⊑ c 1 ⊑ (c 1 ⊔ y) = (c ′ 1 ⊔ b ′′ ⊔ y) = (c ′ 1 ⊔ α). Again, this would mean that (α, β) is irrelevant in M( P, c ), a contradiction, therefore d ′ = β. Hence, we know that Q, d α =⇒ Q ′ , β then by Proposition 6 (α, β) ∈ M( Q, d ). Fi- nally, let us assume by contradiction that (α, β) is irrelevant in M( Q, d ). Then there exists (α 1 , β 1 ) ∈ M( Q, d ) such that (α 1 , β 1 ) (α, β), namely α 1 ⊑ α (equivalently ∃z ′ .α 1 ⊔ z ′ = α) and β ⊑ α ⊔ β 1 . By Proposition 7 we have that Q, d ⊔ α 1 -→ * Q 1 , β 1 , then (α 1 , β 1 ) ∈ Q, d
(α ⊔ c ′ 2 ) = (α 1 ⊔ z ′ ⊔ c ′ 2 ) = (a ⊔ b 1 ⊔ z ′ ⊔ c ′ 2 ) = (c 2 ⊔ z ′ ) and since β 1 ⊑ c 2 and α ⊑ c 2 then β ⊑ (α⊔β 1 ) ⊑ (c 2 ⊔z ′ ) = (α⊔c ′
2 ). Once again, this would mean that (α, β) is irrelevant in M( P, c ), a contradiction. Finally, we can conclude that (α,

β) is relevant in M( Q, d ) therefore (α, β) ∈ M C ( Q, d ).
Using the these Lemma 6 and 7 we conclude the following theorem.

Theorem 6. P, c = Q, d iff M C ( P, c ) = M C ( Q, d )
By combining Theorem 5 and Theorem 6 we get a simple decision procedure for ≈sb by reducing weak saturated equivalence between two given configuration to the set equivalence of the corresponding compact input-output representations. The complexity of this procedure is clearly determined by the complexity of constructions of the compact input-output sets. Proof. The first item follows from Theorem 5 and Theorem 6 and the second item is derived from the construction of M C (γ) and M C (γ ′ ).

Improving the partition refinement for CCP

In this section we show that in the general case of CCP systems, the strategy from Section 4.2 can be used for their CCP\+ components, thus producing a IS ⋆ which may be significant smaller (although the worst case remains exponential).

Given a configuration γ the idea is to detect when an evolution of γ, i.e. a γ ′ s.t. γ

α 1 =⇒ . . . α k =⇒ γ ′ ,
is a CCP\+ configuration. This way we can avoid adding new configurations with Rule (RD IS ) whenever γ ′ ∈ Conf CCP\+ , and redundancy can be then checked using Proposition 3. Using this algorithm we can decide ≈sb in a more efficient manner, although, in the worst-case scenario, still with exponential time. This follows from Proposition 3 and Theorem 1. 3) and self-loops are omitted.

(IS' =⇒) γ ∈ IS γ ∈ IS ⋆ (RS' =⇒) γ ∈ IS ⋆ γ α γ ′ γ ′ ∈ IS ⋆ (opt-RD =⇒) γ ∈ IS ⋆ γ ∈ Conf CCP\+ t 1 = γ α P 1 , c 1 t 2 = γ β P 2 , c 2 α ⊏ β c 2 = c 1 ⊔ β P 1 , c 2 ∈ IS ⋆
Theorem 8. Let γ and γ ′ be two CCP configurations. Let IS = {γ, γ ′ } and let P be the output of imp-weak-pr-ccp(IS , =⇒) in Definition 15. Then

• γ P γ ′ iff γ ≈sb γ ′ .
• imp-weak-pr-ccp(IS , =⇒) may take exponential time in the size of Config -→ (IS ).

It is clear that it is better to use imp-weak-pr-ccp(IS , =⇒) instead of weak-pr-ccp(IS , =⇒) since the new procedure avoids adding new states whenever they are not necessary to check redundancy w.r.t. ≈sb . In other words, if a configuration has subcomponents which do not use the nondeterministic choice then we can take advantage of this by efficiently deleting their redundant transitions.

Unfortunately, this improvement does not escape from the worst-case scenario of weak-pr-ccp(IS , =⇒). Nevertheless, this approach shows the applicability of the strategy developed in Section 4.2. One may expect a practical impact of this optimization since most configurations are composed by several CCP\+ subconfigurations. We want to conclude this section by pointing to Figure 5 which illustrates the main advantage of using this method.

Congruence issues

A typical question in the realm of process calculi, and concurrency in general, is whether a given process equivalence is a congruence. In other words, whether the fact that P and Q are equivalent implies that they are still equivalent in any context. More precisely, an equivalence ∼ = is a congruence if

P ∼ = Q implies C[P ] ∼ = C[Q]
for every process context C. Intuitively, a context C is an expression with a hole • such that replacing • with a process yields a process term. The expression C[P ] denotes the process that results from replacing in C, the hole • with P . For example C = R • then C[P ] = R P .

The congruence issue is fundamental for algebraic as well as practical reasons; one may not be content with having P ∼ = Q equivalent but R P ∼ = R Q. Nevertheless, some of the representative equivalences in concurrency are not congruences. For example, in CCS [START_REF] Milner | A Calculus of Communicating Systems[END_REF], trace equivalence and strong bisimilarity are congruences but weak bisimilarity is not because it is not preserved by summation contexts. So given a notion of equivalence one may wonder in what contexts the equivalence is preserved. For instance, the problem with weak bisimilarity can be avoided by using a somewhat less liberal summation called guarded-summation (see [START_REF] Milner | Communicating and mobile systems: the π-calculus[END_REF]).

In this section we show that weak (saturated barbed) bisimilarity ( ≈sb ) is a congruence for the main CCP fragment here considered; CCP\+. We also show that ≈sb is not a congruence for the full language of CCP. Moreover, unlike CCS, we shall see that restricting the syntax to guarded summation will not prevent the problem. In fact, our counterexample reveals that the problem is intrinsic to CCP. Despite the negative result for the full language, here we also show that weak bisimilarity is still a useful notion: its underlying co-inductive technique (bisimulation) as well as the verification algorithms we introduced in previous sections can be used to establish the standard observational equivalence in CCP. More precisely, we will show that ≈sb implies observational equivalence in CCP, and hence it give us a semi-decision procedure for the standard equivalence of CCP.

Observational Equivalence

The standard notion of observables for CCP are the results computed by a process for a given initial store. More formally, given a (maximal) computation ξ of the form:

Q 0 , d 0 -→ Q 1 , d 1 -→ . . . -→ Q n , d n -→ the result of ξ, denoted by Result(ξ), is the final store d n .
We shall say then that two configurations are observational equivalent if they produce the same set of outputs when given the same input. More formally: In [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF][START_REF] Hofmann | Bisimulation Techniques and Algorithms for Concurrent Constraint Programming[END_REF] it was shown that, in CCP\+, weak saturated barbed bisimilarity and observation equivalence coincide. Recall that P ≈sb Q means P, true ≈sb Q, true . Theorem 9. ( [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF][START_REF] Hofmann | Bisimulation Techniques and Algorithms for Concurrent Constraint Programming[END_REF]) Let P and Q be CCP\+ processes. Then P ∼ o Q if and only if P ≈sb Q.

Nevertheless, the above theorem does not hold for the full language of CCP. We can show this by using a counter-example reminiscent from the standard one for CCS. Namely, in CCS one can prove that, in general, a + τ.P is not weakly bisimilar to a + P . We can use a similar approach for CCP as follows. However, the "if" direction of the theorem does hold. We show this next.

.t. α ∈ O(P )(d) but α ∈ O(Q)(d). Hence P, d -→ * P ′ , α -→ however there is no Q ′ s.t. Q, d -→ * Q ′ , α -→. Therefore, for each computation Q, d -→ * Q ′ , β -→ we have that either (i) β ⊏ α, (ii) α ⊏ β or (iii) β ⊑ α.
We shall prove that there is no saturated barbed bisimulation R containing the pair P ′ , α R Q ′ , β for any of the three cases of β. First, consider the computations of type (i). Notice that since Q ′ , β -→ and β ⊏ α then Q ′ , β ⇓ α while P ′ , α ⇓ α . Now take the type (ii) and this time Q ′ , β ⇓ β but P ′ , α ⇓ β since α ⊏ β. Similarly, in the type (iii) computations we have that Q ′ , β ⇓ α however P ′ , α ⇓ α . From these three cases we can conclude that P ′ , α cannot be related with Q ′ , β in R. Finally, in order to match P ′ , α ⇓ α then the only case left would correspond to Q

, d -→ * Q ′ , α -→ * Q ′′ , α ′ with α ⊏ α ′ , but again Q ′ , α ⇓ α ′ while P ′ , α ⇓ α ′ .
Since Q, d is not able to match P, d -→ * P ′ , α then there cannot be weak saturated barbed bisimulation relating P, d and Q, d , a contradiction to the hypothesis P ≈sb Q.

Therefore, we can use the algorithms presented in this paper as semi-decision procedures for observational equivalence. We can also use the co-inductive technique of weak saturated barbed bisimulation to establish observational equivalence: I.e., if we can exhibit a weak saturated barbed bisimulation containing the pair P, true and Q, true then P ∼ o Q.

Congruence

We begin by showing that weak bisimilarity is a congruence in a restricted sense: It is preserved by all the contexts from the summation-free fragment. For this purpose it is convenient to recall an equivalent definition of weak bisimilarity introduced in [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF][START_REF] Hofmann | Bisimulation Techniques and Algorithms for Concurrent Constraint Programming[END_REF].

Definition 17. (Weak bisimilarity) A weak bisimulation is a symmetric relation R on configurations such that whenever

(γ 1 , γ 2 ) ∈ R with γ 1 = P, c and γ 2 = Q, d : (i) if γ 1 ↓ e then γ 2 ⇓ e , (ii) if γ 1 α -→ γ ′ 1 then ∃γ ′ 2 s.t. Q, d ⊔ α -→ * γ ′ 2 and (γ ′ 1 , γ ′ 2 ) ∈ R.
We say that γ 1 and γ 2 are weakly bisimilar, written γ 1 ≈ γ 2 , if there exists a weak bisimulation R such that (γ 1 , γ 2 ) ∈ R. We write P ≈ Q iff P, true ≈ Q, true .

The following theorem from [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF][START_REF] Hofmann | Bisimulation Techniques and Algorithms for Concurrent Constraint Programming[END_REF] states that the above equivalence coincides with weak saturated barbed bisimilarity (Definition 4). Theorem 11. ([8,[START_REF] Hofmann | Bisimulation Techniques and Algorithms for Concurrent Constraint Programming[END_REF]) ≈sb = ≈.

Using these definitions we can now prove that ≈sb is a congruence in CCP\+.

Theorem 12. Let P, Q and R be CCP\+ processes and assume that P ≈sb Q. Then

1. (ask (c) → P ) ≈sb (ask (c) → Q), 2. (P R) ≈sb (Q R).
Proof. We will focus on the parallel operator since the ask case is trivial. We shall prove that R For proving the part (b) of the above claim, we let R = (ask (e) → tell(α))+ (ask (e) → tell(β)). We shall prove that no weak bisimulation can contain the pair ( P R, e , Q R, true ). The results then follows from Theorem 11 and the fact that P ′ R, true ≈sb P R, e which can be easily verified. Consequently, let us assume that P R, e -→ P tell(α), e by executing the left summand of R. By condition (ii) of weak bisimulation Q R, true must match the move. We have two cases:

= {( P R, c , Q R, d ) | P, c ≈ Q, d }
• Q R, true does not make a transition. And now let us suppose that Q R, true e -→ Q tell(β), true . This means that P tell(α), e now has to match this transition. However Q tell(β), true -→ Q, β ⇓ β while P tell(α), e ⇓ β . Thus we cannot satisfy condition (i) of weak bisimulation.

• Q R, true makes a transition. To match the move it should also execute the left summand of R. However, since e is not the store of Q R, true , Q must be executed first. and this means executing of one of summands in Q to be able to add e to the store. If the left summand of Q is executed, we get Q R, true -→ * tell(α), c⊔e . In this case we could then take the move P tell(α), e -→ tell(d) tell(α), e . But then tell(α), c⊔e ⇓ c and notice that tell(d) tell(α), e ⇓ c , thus we cannot satisfy condition (i) of weak bisimulation. The case where the right summand of Q is executed is symmetric.

Conclusions and Future Work

In this paper we explored the use of the partition refinement algorithm for CCP from [START_REF] Aristizábal | Partition refinement for bisimilarity in CCP[END_REF] and [START_REF] Pino | Weak CCP bisimilarity with strong procedures[END_REF] for checking observational equivalence in the CCP\+ fragment. In [START_REF] Aristizábal | Partition refinement for bisimilarity in CCP[END_REF] authors gave a decision procedure for ∼sb and in [START_REF] Pino | Weak CCP bisimilarity with strong procedures[END_REF] authors proved how the algorithm for ∼sb can be used to compute ≈sb . In this paper, we proved that this procedure takes exponential time and space (in the size of the set of reachable configurations) even for the restricted case of CCP\+. We then proposed two alternative methods for checking observational equivalence in CCP\+ by exploiting some of the intrinsic properties of this fragment, in particular confluence. We proved that both procedures take polynomial time (in the size of the set of reachable configurations), thus significantly improving the exponential-time approach from [START_REF] Aristizábal | Partition refinement for bisimilarity in CCP[END_REF][START_REF] Pino | Weak CCP bisimilarity with strong procedures[END_REF], which is, to the best of our knowledge the only algorithm for checking observational equivalence in CCP. Each of the two method has its advantages over the other. On the one hand, the algorithm from Section 4 uses significantly more time and space than the one from Section 5, however it can be easily adapted for for full language of CCP as shown in Section 6. On the other hand, the procedure from Section 5 takes less time and uses only linear space nevertheless there is no "trivial" adaptation for the full language as it does not rely on the partition refinement approach. We also studied congruence issues for ≈sb for CCP\+ and CCP as well as the relationship between ≈sb and observational equivalence.

From a theoretical perspective, it would be interesting to lift such relationship to the whole CCP including recursive definitions: these allow infinite computations for which the notion of observation requires fairness [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF]. In [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF], we have shown that these notions coincides for CCP\+ but, for the whole calculus a better understanding is missing. From a more practical point of view, we would like to proceed with an experimental evaluation comparing the performances of the various approaches that we have discussed in this paper. Furthermore we would like to consider more efficient partition refinement algorithms [START_REF] Dovier | An efficient algorithm for computing bisimulation equivalence[END_REF] to check whether the algorithm from Section 4 can be further improved. The challenge would be to find a more efficient version of =⇒ that can still be used for deciding ≈sb and so it can be adapted to the case of the full CCP. Finally, we plan to investigate how the procedures here defined can be extended to different versions of CCP where the summation operator is not present, for instance timed CCP (tcc) [START_REF] Saraswat | Foundations of timed concurrent constraint programming[END_REF], universal temporal CCP (utcc) [START_REF] Olarte | Universal concurrent constraint programing: symbolic semantics and applications to security[END_REF] and epistemic CCP (eccp) [START_REF] Knight | Spatial and epistemic modalities in constraint-based process calculi[END_REF].

Figure 1 :

 1 Figure 1: An example of the use of F (P) from Equation1

Example 4 .

 4 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. The LTSs of γ 1 and γ 2 are the following: γ 1 -→ stop, true and γ 2 c -→ tell(d), c -→ stop, c . It is now easy to see that the symmetric closure of the relation

Figure 2 :Example 5 .Example 6 . 2 c-

 2562 Figure 2: LTS -→ ({ R ′ + S, true , S, true , R + S, true , P, z < 5 }).

Example 7 .

 7 Consider the following process: P = (ask (x < 15) → tell(y > 42)) + (ask (x < 10) → tell(y > 42))

(

  ask (a) → stop) + (ask (b) → stop), true stop, a stop, b (ask (a) → stop), true stop,

Figure 3 :

 3 Figure 3: An example of the use of IR -→ (P) as in Definition 7. Let a ⊏ b, notice that γ 1 and γ 2 end up in the same block after the refinement since γ 1 b -→ γ b1 is a redundant transition w.r.t P hence it is not required that γ 2 matches it.

  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 7 Termination If P n = P n+1 then return P n .

Algorithm 3

 3 weak-pr-ccp(IS , ) Initialization 1. Compute IS ⋆ with the rules (IS IS ), (RS IS ), (RD IS ) defined in Table 4, 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 7 Termination If P n = P n+1 then return P n .

Figure 4 :

 4 Figure 4: LTS -→ (IS ) where IS = { P n , true } as in Example 9. The configurations in the right part are generated by (RD IS -→ ) applied to the source nodes of the dotted arrows. Some transitions and stop processes were omitted for clarity.

Lemma 4 .

 4 Let γ ∈ Conf CCP\+ . For all γ ′ ∈ Deriv(γ) we have γ ≈sb γ ′ . Proof. Let R = {(γ 1 , γ 2 ) | ∃γ 3 s.t. γ 1 -→ * γ 3 and γ 2 -→ * γ 3 },we prove that R is a weak saturated barbed bisimulation. Let (γ 1 , γ 2 ) be any pair of configurations in R.

( i )

 i If γ 1 ⇓ e then by definition γ 1 -→ * γ ′ 1 ↓ e . By confluence (Proposition 2) γ ′ 1 -→ * γ 3 and thus γ 3 ↓ e (since constraints can only be added). Since γ 2 -→ * γ 3 ↓ e we conclude that γ 2 ⇓ e . (ii) If γ 1 -→ * γ ′ 1 , then by confluence γ ′ 1 -→ * γ 3 and therefore (γ ′ 1 , γ 2 ) ∈ R. (iii) Finally, let γ 1 = P 1 , c 1 and γ 2 = P 2 , c 2 . If P 1 , c 1 -→ * P 3 , c 3 and P 2 , c 2 -→ * P 3 , c 3 , then P 1 , c 1 ⊔ e -→ * P 3 , c 3 ⊔ e and P 2 , c 2 ⊔ e -→ * P 3 , c 3 ⊔ e and thus ( P 1 , c 1 ⊔ e , P 2 , c 2 ⊔ e ) ∈ R.

Lemma 5 .

 5 (Soundness) If P, c α =⇒ max P ′ , c ′ then P, c ⊔ α =⇒ max P ′ , c ′ . (Completeness) If P, c ⊔ a =⇒ max P ′ , c ′ then there exists α and b such that P, c α =⇒ max P ′ , c ′′ where α ⊔ b = a and c ′′ ⊔ b = c ′ .

Algorithm 4

 4 weak-pr-dccp(IS ) Initialization1. Compute G = LTS =⇒max (IS ) using the rules (IS IS =⇒max ) and (RS IS =⇒max ), 2. G ′ = remRed(G)where the graph remRed(G) results from removing from G the redundant transitions w.r.t. ≈sb ,3. P 0 = {B 1 } . . . {B m } is a partition of V(G ′ )where γ and γ ′ are in B i iff they satisfy the same weak barbs (⇓ e ),

Theorem 4 .

 4 Let γ and γ ′ be two CCP\+ configurations. Let IS = {γ, γ ′ }, let P be the output of weak-pr-dccp(IS ) in Algorithm 4 and let N = |Config -→ (IS )|. Then• γ P γ ′ iff γ ≈sb γ ′ .• weak-pr-dccp(IS ) takes O(N 3 ) time and uses O(N 2 ) space.Proof. The first item follows from the Theorem 2 and Proposition 3. As for the second item:(Step 1) G = LTS =⇒max (IS ) takes O(N 2) time and space since =⇒ max will add, at most, a transition from each element in V(G) to every other configuration in V(G) and |V(G)| = |Config -→ (IS )| = N . (Step 2) Each node in V(G) has at most N -1 outgoing transitions, then G ′ = remRed(G) takes O((N -1) * (N -1)) = O(N 2 ) per node, thus this step takes O(N 2 * N ) = O(N 3 ) time. (Step 3) P 0 can be created in O(N 2 ) by definition of =⇒ max . (Iteration) Using the procedure from Tarjan et al. [29], this step takes O(|E| log |V |) time and uses O(|E|) space. Therefore, since |V(G)| = N and |E(G)| = O(N 2 ), hence we have O(N 2 log N ) and O(N 2 ) space. We can conclude that weak-pr-dccp(IS ) takes O(N 3 ) time and uses O(N 2 ) space.

Definition 10 .

 10 (Barb equivalence) P, c and Q, d are (weak) barbed equivalent, written P, c ∼ wb Q, d , iff ∀e, α ∈ Con 0 . P, c ⊔ e ⇓ α ⇔ Q, d ⊔ e ⇓ α Let us give an example. Example 10. Let P = tell(true) and Q = ask (c) → tell(d). We can show that P, true ∼ wb Q, true when d ⊑ c (as in Example 4). One can check that for all c ′ we have P, c ′ ⇓ c ′ and Q, c ′ ⇓ c ′ . Notice that whenever c is entailed then tell(d) does not add any more information since d ⊑ c. The full characterization of ≈sb in terms of weak-barbed equivalence is given next. Notice that the following theorem uses Lemma 4 which itself depends on the confluent nature of CCP\+. Theorem 5. Let P, c and Q, d be CCP\+ configurations. P, c ≈sb Q, d iff P, c ∼ wb Q, d Proof. (⇒) Assume that P, c ≈sb Q, d then by condition (i) of ≈sb (Definition 3) we have ∀α ∈ Con 0 . P, c ⇓ α ⇔ Q, d ⇓ α , hence in combination with condition (iii) we can conclude P, c ⊔ e ⇓ α ⇔ Q, d ⊔ e ⇓ α . (⇐) Let R = {( P, c , Q, d ) | ∀e, α ∈ Con 0 . P, c⊔e ⇓ α ⇔ Q, d⊔e ⇓ α }, we prove that R is a weak saturated barbed bisimulation: (i) Take e = true then ∀α ∈ Con 0 . P, c ⇓ α ⇔ Q, d ⇓ α . (ii) Assume that P, c -→ * P ′ , c ′ , by Lemma 4 P, c ≈sb P ′ , c ′ hence by (⇒) we can conclude that P ′ , c ′ R Q, d . (iii) Assume P, c R Q, d then for all e ′ we have P, c ⊔ e ′ R Q, d ⊔ e ′ just by taking e = e ′ . We shall show a compact representation of the set of weak barbs of a configuration under any possible context. First we introduce some convenient notation for this purpose. The set P, c will contain pairs of the form (α, e). Definition 11. (Input-Output set) The input-output set of a given configuration P, c is defined as follows: P, c def = {(α, e) | P, c ⊔ α ⇓ e } Let us give an example. Example 11. Let γ = ask a → tell(b), true where b ⊑ a. γ = {(α, α)|α ⊏ a or a ⊑ α} ∪ {(β, β ⊔ b)|a ⊑ β}

Corollary 1 .

 1 P, c = Q, d iff P, c ∼ wb Q, d Proof. (⇒) Assume (β, a) ∈ P, c then P, c ⊔ β ⇓ a . Hence, we can take e = β and by hypothesis Q, d ⊔ β ⇓ a therefore (β, a) ∈ Q, d . (⇐) Assume that P, c ⊔ β ⇓ a for some β and a, then (β, a) ∈ P, c and by hypothesis (β, a) ∈ Q, d therefore by definition Q, d ⊔ β ⇓ a .

Proposition 4 .Proposition 5 .

 45 Let (α, e) ∈ P, c . If (α, e) (β, e ′ ) then (β, e ′ ) ∈ P, c . Proof. By definition P, c ⊔ α ⇓ e then by monotonicity P, c ⊔ β ⇓ e⊔β so P, c ⊔ β ⇓ e ′ since e ′ ⊑ (e ⊔ β), therefore (β, e ′ ) ∈ P, c . Moreover, the relation is well-founded. More precisely, There is no infinite strictly descending chain p 1 ≻ p 2 ≻ . . . . Proof. Follows from the well-foundedness of ⊑ (Remark 1).

Definition 14 .

 14 (Compact input-output set) The compact input-output set of a configuration P, c is defined as follows: M C ( P, c ) def = {(α, e) | (α, e) ∈ M( P, c ) and (α, e) is relevant in M( P, c )} Let us give an example. Example 14. Let γ and γ ′ as in Example 13. Using the same reasoning as in Example 12 one can check that:

Proposition 7 . 1 -

 71 If (α, e) ∈ M( P, c ) then P, c ⊔ α -→ * P ′ , e Proof. By definition of M( P, c ), since (α, e) ∈ M( P, c ) then there exist α 1 , . . . , α n such that α = n i=1 α n and P, c α → . . . αn -→ P ′ , e . Hence by soundness on each transition P, c ⊔ n i=1 α n = P, c ⊔ α -→ * P ′ , e .

  Thus, this would mean that (α, β) is irrelevant in M( P, c ), a contradiction, therefore α ′ = α and by consequence d ′′ = d ′ . Therefore, we know thatQ, d α =⇒ Q ′ , d ′ , now let us assume by contradiction that d ′ = β (i.e. β ⊏ d ′ ).By soundness and Lemma 3 we have thatQ, d ⊔ α -→ * Q ′ , d ′ , this means that (α, d ′ ) ∈ Q, d. By hypothesis then (α, d ′ ) ∈ P, c so there exist P 1 , c 1 s.t. P, c ⊔ α -→ * P 1 , c 1 and d ′ ⊑ c 1 . By Lemma 3 then P, c ⊔ α =⇒ P 1 , c 1 , now by completeness, there exist y, b ′′ s.t. P, c y =⇒ P 1 , c ′ 1 where y ⊔ b ′′ = α and c ′ 1 ⊔ b ′′ = c 1 . Using Lemma 6 we get that (y, c ′ 1 ) ∈ M( P, c ). Now let us prove that (y, c ′ 1 ) (α, β), namely y ⊑ α and β ⊑ (α ⊔ c ′ 1

  and by hypothesis (α 1 , β 1 ) ∈ P, c . This means that P, c⊔α 1 -→ * P 2 , c 2 where β 1 ⊑ c 2 , now by Lemma 3 we get P, c ⊔ α 1 =⇒ P 2 , c 2 . By completeness of =⇒ there exist a, b 1 s.t. P, c a =⇒ P 2 , c ′ 2 where (a⊔b 1 ) = α 1 and (c ′ 2 ⊔b 1 ) = c 2 . Hence, by Proposition 6 we know that (a, c ′ 2 ) ∈ M( P, c ). Now let us prove that (a, c ′ 2 ) (α, β) namely a ⊑ α and β ⊑ (α ⊔ c ′

Theorem 7 .

 7 Let γ and γ ′ be two CCP\+ configurations. Let IS = {γ, γ ′ } and letN = |Config -→ (IS )|. Then • M C (γ) = M C (γ ′ ) iff γ ≈sb γ ′ . • Checking whether M C (γ) = M C (γ ′ ) takes O(N 2 ) time and uses O(N )space.

(Figure 5 :

 5 Figure5: The above example illustrates the advantages of using the method discussed in Section 6: only the dashed transitions need to be taken into account to check ≈sb . Transitions are computed according to =⇒ (Table3) and self-loops are omitted.

Definition 16 .

 16 (Observational equivalence) Let O : Proc → Con 0 → 2 Con 0 be given by O(P )(d) = {e | P, d -→ * P ′ , e -→}. We say that P and Q are observational equivalent, written P ∼ o Q, iff for all d, O(P )(d) = O(Q)(d).

Claim 1 .

 1 There are P, Q s.t. P ∼ o Q but P ≈sb Q. Proof. Let P = (ask (b) → tell(c)) + (ask (true) → ask (d) → tell(e)) and Q = (ask (b) → tell(c)) + (ask (d) → tell(e)) for unrelated elements b, c, d, e ∈ Con 0 . It is straightforward to see that P ∼ o Q since the only relevant inputs are true, b and d for which both processes produce true, c and e respectively. Now let us show that P ≈sb Q. First notice that if we take the transition P, true -→ ask (d) → tell(e), true then Q, true can only stay still. Now if we take the transition Q, true b -→ tell(c), b then note that tell(c), b ⇓ c but ask (d) → tell(e), b ⇓ c . Hence P ≈sb Q.

Theorem 10 .

 10 If P ≈sb Q then P ∼ o Q. Proof. Let us assume by means of contradiction that P ≈sb Q and there exists d s.t. O(P )(d) = O(Q)(d). By definition, this means that there is an α s

  is a weak bisimulation (Definition 17). The result then follows from Theorem 11.

  (i) Assume that P R, c ↓ α then, since P, c ≈ Q, d , by condition (i) we have that Q R, d ⇓ α .(ii) Now suppose that P R, c α -→ P 1 , c 1 for some P 1 , c 1 . By induction on (the depth) of the inference of P R, c α -→ P 1 , c 1 we have the following two cases:• Using Rule LR3 (left) we have that P R, c α -→ P ′ R, c ′ , hence P, c α -→ P ′ , c′ by a shorter inference. Using this transition and the hypothesis in R we can conclude thatQ, d ⊔ α -→ * Q ′ , d ′ and P ′ , c ′ ≈ Q ′ , d ′ (1). Now using Rule LR3 we get that Q R, d ⊔ α -→ * Q ′ R, d ′and, because of (1), we know thatP ′ R, c ′ R Q ′ R, d ′ . • Using Rule LR3 (right) we have that P R, c α -→ P R ′ , c ′ , hence R, c α -→ R ′ , c ′ by a shorter inference, where c ′ = c ⊔ α ⊔ β. Given that P, c ↓ c then by the hypothesis we know that Q, d ⇓ c . This means that Q, d -→ * Q ′ , d ′ ↓ c ,moreover by Lemma 4, Theorem 11 and the hypothesis we can conclude that Q, d ≈ Q ′ , d ′ ≈ P, c . Therefore Q R, d⊔α -→ * Q ′ R, d ′ ⊔α since c ⊑ d ′ . Now from this transition notice that Q ′ R, d ′ ⊔ α -→ * Q ′ R ′ , d ′ ⊔ α ⊔ β and it is the case that Q ′ R ′ , d ′ ⊔ α ⊔ β R P R ′ , c ⊔ α ⊔ β since Q ′ , d ′ ≈ P, c .Unfortunately, due to summation, the second point in the theorem above does not hold for arbitrary CCP processes. Claim 2. There are P ′ , Q, R such that (a) P ′ ≈sb Q and (b)(P ′ R) ≈sb (Q R).To prove this claim we let P = (ask (true) → tell(c)) + (ask (true) → tell(d)), P ′ = P tell(e) and Q = (ask (true) → tell(c⊔e))+(ask (true) → tell(d⊔e)) with c ⊑ d, c ⊑ e, d ⊑ c, d ⊑ e, e ⊑ c, e ⊑ d. For (a) we can show that P ′ , true ≈sb P, e ≈sb Q, true . The first equation is trivial. For the second we define a relation on configurations R. The set of pairs in R are those linked in Figure6. It can easily be verified that (the symmetric closure of) R is a weak bisimulation (seeDefinition 17). The point (a) then follows from Theorem 11.

Figure 6 :

 6 Figure 6: Let P = (ask (true) → tell(c))+(ask (true) → tell(d)) and Q = (ask (true) → tell(c ⊔ e)) + (ask (true) → tell(d ⊔ e)). The linked configurations are weakly bisimilar.

Table 1 :

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

Table 4 :

 4 Rules for generating the states used in the partition refinement for CCP Example 8. Consider the following processes:

Table 5 :

 5 Rules for improved version of the partition refinement for CCP.Definition 15. (Improved partition refinement for CCP)We define the procedure imp-weak-pr-ccp(IS , ) by using the rules in Table5in Step 1 of weak-pr-ccp(IS , ) from Algorithm 3.

Preprint submitted to Science of Computer ProgrammingDecember[START_REF] Bonchi | Symbolic semantics revisited[END_REF] 2014

The other can be easily adapted for the full ✩ This work has been partially supported by the project ANR 12IS02001 PACE, ANR-09-BLAN-0169-01 PANDA, and by the French Defense procurement agency (DGA) with a PhD grant.