Generating recommendations for consensus negotiation in group personalization services

There are increasingly many personalization services in ubiquitous computing environments that involve a group of users rather than individuals. Ubiquitous commerce is one example of these environments. Ubiquitous commerce research is highly related to recommender systems that have the ability to provide even the most tentative shoppers with compelling and timely item suggestions. When the recommendations are made for a group of users, new challenges and issues arise to provide compelling item suggestions. One of the challenges a group recommender system must cope with is the potentially conflicting preferences of multiple users when selecting items for recommendation. In this paper, we focus on how individual user models can be aggregated to reach a consensus on recommendations. We describe and evaluate nine different consensus strategies and analyze them to highlight the benefits of group recommendation using live-user preference data. Moreover, we show that the performance is significantly different among strategies.

Introduction
Personalization services in ubiquitous environmentsubiquitous personalization services computing-has recently been emerging in many areas of society [25,46,47]. Ubiquitous commerce is one of these areas. In ubiquitous commerce, in order to support personalization services, a system should recognize preferred products (i.e., also known as items) through preference analysis such as a personal profile. Research on ubiquitous commerce has come up with a number of recommendation systems reaching out in the real world.
Recommender Systems are particularly well adapted to e-commerce applications where users need to be guided through complex product spaces. They combine user profiling and filtering techniques to provide more proactive and personal information retrieval systems, and have been gaining in popularity as a way of overcoming the ubiquitous information overload problem. Much of the research on ubiquitous recommendation systems are related to mobile phones and have been examined under the term m-commerce [49]. Examples include: a ubiquitous shopping system called MyGROCER [24], MovieLens Unplugged (MLU) [34], Mobile Sales Assistant [40], Buying-net [23], and APriori [38] product recommendation system. Apart from m-commerce applications, a great number of ubiquitous computing applications also apply recommendation systems. For example, there have been numerous works on recommending tourist attractions (e.g., COMPASS [43]) or more general recommendation algorithms for mobile devices [16].
While much of the research on ubiquitous recommendation systems has focused on making recommendations to the individual [23,39], many scenarios involve groups of inter-related users [17,41]. In these sce-narios, typically a group of people are intending to participate in a group activity [35].
Recently some researchers have begun to look at the whole set of new challenges and issues associated with group recommendation [21]. It is no longer reasonable to generate a set of recommendations with respect to a single set of (relatively) consistent preferences, as is normally the case in the single-user scenario. Instead, groups of users are likely to introduce a diverse range of preferences where conflicting needs are likely to be commonplace and where different users may be more or less easy to satisfy [19].
The job of the group recommender is to make suggestions that reflect the preferences of the group as a whole, while offering reasonable and acceptable consensus options to individual group members. In this regard, a key aspect of group recommendation concerns the way in which individual users profiles are combined to reach a consensus on recommendation (or a set of recommendations) for the group at the completion of the group session.
The work presented in this paper continues previous work [30][31][32] on group recommendation. In particular, this previous work proposed specific group recommendation approaches and focused on interfacing functionality that assists individual group members in better understanding the evolving needs of the group. This helps group members to appreciate the compromises that may be required for a satisfactory conclusion to be reached (see also [20]). From previous work, one remaining unsolved issue is: how to reach a consensus when all users have completed interacting with the system and have chosen their preferred items? The aim of consensus negotiation is to help the group members arrive at a final recommendation which maximally satisfies the individual members preferences. In this paper we focus on the consensus-based recommendation technique, describing and evaluating nine different approaches for reaching a consensus on recommendations. Moreover, we describe the results of an evaluation, based on liveuser data, as a means to explore the relationship between group diversity and consensus recommendation. It is worth mentioning that the proposed strategies start from the premise that each user has an individual user model that contains her preferences. They are defined accordingly to this premise with the aim of being general enough to be applicable to a wide range of group recommender scenarios. Notice that recommender systems can be distinguished by the type of feedback that they support; examples include value elicitation, ratingsbased feedback and preference-based feedback [45]. In particular, we analyze the strategies in a conversational case-based reasoning recommender 1 . We use a form of user feedback called critiquing [5,33], where a user indicates a directional feature preference in relation to the current recommendation. To demonstrate that they are general enough, we compare our proposals with wellknown state-of-the-art approaches normally used for recommendation generation in collaborative filtering.
Hence, the contributions of this work are two-fold. First of all, we propose a set of new strategies for reaching consensus. Second, we evaluate them based on liveuser preference information, in which we compare the performance of different consensus strategies on different groups sizes and different types of user groups, ranging from groups with very similar preferences to more diverse groups with competing preferences.
The rest of this paper is organized as follows. In the next section we review related work on group recommender systems. Section 3 describes our proposed consensus-based recommendation strategies. Section 4 is devoted to a small example that help the reader to understand the proposals. Next, Section 5 discusses the experimental results. Finally, we conclude the paper with a discussion about the main results and implications of the work.

Related work
Ubiquitous computing research has uncovered many new situations where recommendation technology can have a critical role to play, and in many of these situations there may be more than one individual designated as the recipient of the recommendation. For example, the way in which we book a restaurant to go with our families using a mobile environment [36]. Accordingly a group of friends, or family members, now have access to hundreds of restaurants' content from which to choose. Recommendation technologies will help them to more effectively navigate through this content space, but in doing so must cater for a set of users rather than a single user. These types of scenario have motivated recent interest in group recommendation and to date a variety of early-stage systems have been developed in domains such as group web-page recommendation [26,37,44], recommending vacations or tours to groups of tourists [1,19,31,43], recommending music tracks and playlists to large groups of listeners [8,29], and, recommending movies and TV programmes to friends and family [15,35,48]. Group recommenders can be distinguished, as defined in [21], according to their approach to 4 basic recommendation sub-tasks -(1) preference elicitation; (2) recommendation generation; (3) presentation and explanation; (4) consensus negotiation.
Preference elicitation refers to the manner in which information is acquired from users and in many cases methods similar to those used in single-user recommender systems are applied. For example, preferences may be acquired by asking users directly (explicit preference elicitation) or by inferring their preferences from their actions and feedback (implicit preference elicitation). In the case of the former, systems such as the Travel Decision Advisor [19] and PolyLens [35] both acquire preferences by asking users to specify them explicitly; either in the form of preferred features or item ratings. In contrast, group systems such as FlyTrap [8] and Let's Browse [26] acquire the preferences by monitoring a user's interactions. FlyTrap, for example, learns about the preferences of individual users by mining each user's personal music usage habits. In ubiquitous computing explicit and implicit preference elicitation can be applied [3,39]. Most of the ubiquitous recommender systems use ratings, for example Buying-net [23]. In [22], apart from acquiring explicit preferences, the ubiquitous recommender additionally learns user preferences through learning from the user profile. In this work, the consensus-based proposals are devoted to be applicable to both: explicit and implicit preference elicitation.
Most of the research on group recommendation investigated the core algorithms used for recommendation generation. Two different strategies have been mostly used for generating group recommendations: aggregating individual predictions into group predictions (aggregated predictions) or aggregating individual models into group models (aggregated models). Differences among these strategies differ in the timing of data aggregation step. The aggregated predictions strategy [4,27] generated individual predictions based on individual preference models and then aggregates the individual predictions into a group prediction. The alternative strategy is to construct a group preference model prior to any item recommendation taking place [42]. The aggregated models strategy merges individual user models into a group-based model and then generates recommendations using the aggregated group model [31]. For example, GMK (Group Knowledge Management) [9] proposes a generic framework for management in contextaware group applications and services that extracts group knowledge regarding the involved users.
The final two subtasks (presenting and explaining recommendations and helping group members to reach consensus) have received less attention from researchers. That said, there is an increasing interest in these areas. This is particularly evident in group recommenda-tion scenarios because convincing group members that a particular recommendation is right for them is especially important. For instance, Let's Browse [26] explains its Web page recommendations to group members by highlighting keywords from the page that are judged to be relevant to the group as a whole.
As highlighted in [21], many group recommenders do not explicitly support consensus negotiation. Very often it is assumed that one particular group member is responsible for the final decision; Let's Browse [26], makes this assumption, because one group member typically controls the system interaction with other group members playing the role of viewers rather than actors. Alternatively the role of the recommender could be to produce a set of recommendations that will ultimately be debated by the group offline, before a consensus is reached. In general, consensus remains an open issue for group recommenders. This paper proposes more active solutions to help users to reach consensus in a postrecommendation phase.

Consensus-based strategies
In this section, we propose different strategies to reach a consensus on the recommendations made for a group of users. First, we define some required definitions. Second, we present the consensus strategies divided into three groups: (1) Statistical dispersion strategies; (2) Individual content strategies; and (3) Collaborative filtering strategies. Note that statistical and content dispersion strategies are the proposals of this paper. Additionally, in this section we have also added the explanation of the state-of-the-art strategies commonly used in collaborative filtering algorithms for generating recommendations. We also consider how they can be applied when reaching consensus.

Required definitions
Let P = {p 1 , ..., p n } be a set of products or items for recommendation, where p i is the ith product. Depending on the recommender algorithm, P will be the whole set of products or a subset of them.
Let U = {u 1 , ..., u k } be a set of users, where u j represents the jth user and k the number of users, |U | = k. The set of individual user models will be defined as IM = {IM u1 , ..., IM u k }, where IM uj represents the individual user model of the jth user. We consider that each user u j has an individual user model IM uj = {I 1 , ..., I ru j } that represents her individual preferences, from her initial preference I 1 to her last preference I ru j . Note that the subindex r uj may be different for each user in U because each user defines her own set of preferences. Thus, R is the total number of preferences for the group which is computed as In subsequent sections we will use the satisfaction measure, as defined in Equation 1.
The satisfaction measure, δ(p i , IM uj ), shows for a particular product p i and a user u j , the number of preferences from her individual user model IM uj that product p i satisfies. The parameter w s is a weighting factor that can be used to tune preferences. The Satisf ies(p i , I s ) function depends on the type of feedback the recommender supports. Let's describe a couple of examples: (1) In a content-based recommender system that uses critiquing-based feedback, this measure computes whether a critique 2 is satisfied by product p i ; (2) In a collaborative filtering recommender that uses ratings-based feedback, this measure directly returns the rating 3 value.
Next, we define different strategies for reaching a consensus in a group recommender system. The consensus recommended product or products -i.e., it also depends on the recommender-to a group is generated according to equation 2.
where strategy refers to the name of the strategy.

Statistical dispersion
In this section we propose two strategies, called mean and purity, based on the measurement of dispersion used in statistics and probability theory. The first consensus-based proposal of this paper is called mean. The mean satisfaction, m(p i , IM ), of the group for a product, p i , is defined as the sum of each member, u j , individual satisfaction according to her preferences, IM uj .
The aim of Equation 3 is simply to offer a mean or average to derive a central tendency of the preference We use the sample standard deviation, d(p i , IM ), as defined in Equation 4. It shows the deviation in the satisfaction of the users. A low measure indicates that the preferences tend to be close to the mean and a high value indicates that the preferences are spread out over a large range of values.
Purity is the second strategy of dispersion proposed in this paper, see Equation 5. Roughly, it measures the percentage of positive preferences among the whole set of preferences made by the group that are covered by the product.
A value purity(p i , IM ) = 1, means that all members of the group satisfy their preferences whereas a value purity(p i , IM ) = 0, denotes that none of the preferences of the group are satisfied. This strategy owes its name to a similar measure broadly used in rule-based learning [12]. It has commonly been used to find a rule that covers as many positive examples while covering as few negative examples as possible. The objective of any rule-based algorithm is to find a trade-off between these two conditions using the purity measure in different ways. We have made an adaptation of this measure to group recommender systems. In our case, we measure how many preferences are covered (i.e., satisfied) by a product while considering all the preferences of the group. Moreover, we have included the deviation in the equation to denote the dispersion of the satisfaction.

Individual content
This section describes three individual content strategies named completeness, logical sufficiency and group sufficiency. Individual content dispersion strategies aim at evaluating the individual satisfaction of the members.
The completeness measure has been previously used in negotiation scenarios. For example, in auctions [7] where a buyer and a provider want to reach agreement for the best offer. The negotiation has usually been considered between two individuals. In a group recommendation scenario the negotiation may involve more than two individuals. Thus, Equation 6 has been modified accordingly to group recommenders. The objective of the completeness strategy is to favor high scores while penalizing big differences between members.
where w j is a weighting factor that k j=1 w j = 1 and w j ≥ 0. As defined in Equation 6, the completeness of a product, p i , is computed in terms of members' satisfaction, δ(p i , IM uj ). Moreover, the parameter w j is a weighting factor used to tune the completeness -i.e., to focus more on one of the member's preferences. The sum of √ r uj factors is for normalizing the values in the The degree of logical sufficiency [11] (i.e, in short the ls measure) is a standard likelihood ratio statistic, which has been applied to measure rule quality of rule induction systems. This measure divides the proportion of positive examples that are covered by a rule by the proportion of negative examples. Equation 7 shows this measure adjusted for group recommendation. Given a product, p i , the degree of logical sufficiency of p i with respect to an individual user, u j , is defined as the proportion of satisfaction of u j by the proportion of u j preferences that are not satisfied.
Equation 7 measures the user confidence for a product considering her preferences. Note that a large ls means user u j is widely satisfied by product p i . Note that in the extreme ls approaches to infinity and, in this case, we restrict the value to ls(p i , IM uj ) = δ(p i , IM uj ). On the other hand, if ls is much less than unity, then the product p i is discouraging for user u j . The degree of logical sufficiency of p i for the whole group, ls g , as shown in Equation 8, is defined as the sum of individual logical sufficiency divided by the total number of preferences in the group.
In inductive rule learning algorithms, the ls measure gives rise to the lscontent measure. Equation 9 shows the adaptation to group recommender systems. Essentially, lscontent estimates ls measure with a Laplace correction that penalizes products with low coverage.
When we evaluate the degree of logical sufficiency of a product in relation to an individual member, there is no differences between lscontent and ls. However, lscontent may help to reach a consensus when we apply the degree of logical sufficiency to describe a group sufficiency.
We also propose in this paper a group sufficiency -in short gs-measure based on lscontent. Instead of analyzing the logical sufficiency of a individual member in relation to her satisfied or unsatisfied preferences, gs measures the satisfaction of a member in relation to the satisfied preferences for the rest of the group and to the unsatisfied preferences for the individual in comparison with the whole group. The intuition behind this strategy comes from the fact that the satisfaction of an individual is likely to depend on that of other individual in the group (emotional contagion), as observed by [28].
Equation 10 defines the group sufficiency for a given product p i and a user u j as the proportion of satisfied preferences for user u j in front of the satisfied preferences of the whole group divided by those preferences that have not been satisfied of user u j in front of those unsatisfied for the group. The Laplace correction in this case adds a factor of 1 2 for penalizing products with low coverage. If a product covers no users, its Laplace will be 1 2 . Finally, the degree of group sufficiency of p i is defined as the sum of individual group sufficiency divided by the number of users in the group, see Equation 11. This equation estimates as the best product the one that minimizes gs. Thus, instead of Equation 2, it uses Equation 12.

Collaborative Filtering
In this section we briefly describe the most well-known strategies used in collaborative filtering algorithms for recommendation generation. We argue that they may also be useful for consensus negotiation.
The Least misery strategy, as defined in Equation 13, chooses a product p i based on the minimum satisfaction of the individual preferences. The rationale is that a group is as satisfied as its least satisfied member. PolyLens [35] uses this strategy for a group of people that is going to watch a movie together.
Most pleasure strategy selects the maximum satisfaction of the individual preferences, see Equation 14. It considers that at least one member will be maximally satisfied.
Previous strategies assume the consensus based on the satisfaction of one individual: the least or the most satisfied. There is no warranty that the recommendations will suit the whole group.
Multiplicative strategy multiplies the satisfaction of the individual users, see Equation 15. With this strategy it might happen that a member with unique tastes always lose out because their opinion happens to be a minority preference.
Finally, we describe the Borda count strategy. The Borda count is a voting system divided into two steps. First of all, each individual user ranks the products in order of her individual preferences. Thus, the product p i for individual u j will obtain a rank value that is denoted as rank pi uj . The rank values are computed as follows: (1) Sort out the products according to the satisfaction of the user u j ; (2) Assign to the first product one point, second product receives two points, third product three points and so on. In case there is two or more products with the same satisfaction, the points are averaged and distributed among the products. Second step is devoted to sum rank values obtained for the members of the group, see Equation 16.
The borda count determines the winner product (i.e., the consensus product) by giving each candidate product a certain number of points corresponding to the position it is ranked considering the satisfaction of each user. This strategy has been previously analyzed as a recommendation generation strategy in [2,27].

An illustrative example
To help understand the strategies, we present a simple example to illustrate the consensus-based recommendations suggested by each strategy. We consider the consensus process for a group of four individuals (i.e., U = {P aul, Anne, M ary, John}, then k = 4) and a product base of ten products, P = {A, B, ..., J}. For the sake of simplicity, we consider that all users contains a individual user model with ten preferences (i.e., R = 10+10+10+10 = 40) and that the satisfaction, δ, of these preferences is shown in Table 1. For example, Table 1 shows that Paul and Mary's ten preferences are satisfied with product A, while the same product only satisfies four of Anne's preferences with seven of John's preferences being satisfied. We have also included the sum of preferences satisfied by each product. Looking at product A and F, both satisfy 31 of the group preferences. However, each one of them shows a different satisfaction of the users' preferences. The ls g , gs g and borda count strategies are computed in two phases. First one is devoted to compute a partial result and the second one uses this partial result to obtain a final value. Table 2 shows the results in the first phase for ls, gs and the rank computation of the borda count, respectively.
According to the example described in Table 1, we compute each one of the consensus-based strategies to select a set of products for consensus recommendation 4 . In this example, the set will contain six products. Table 3 shows the results of applying all the consensus strategies. A row indicates for a particular consensus strategy, which is the value obtained when applying the strategy to every one of the products considering all the individual user models. For example, the mean row indicates for product (p i = A) (i.e., see column A) that mean(A, IM ) = 10+4+10+7 4 = 7, 75. Last column in Table 3 depicts the consensus set of products recommended by each strategy. One or more products in parenthesis means that there is a draw between them. Table 3 shows that nearly all strategies select the set of six products in a different order. It is interesting to note that most of strategies agree that H is the best product. However, the second option is not so clear. For example, purity, completeness, most pleasure and multiplicative choose product E and, least misery selects product J.    Additionally, Table 3 also shows that purity and completeness select identical set of products. Coincidences among strategies may happen because this example contains a reduced set of ten products, the size of the group is small and the users are quite similar in their preferences. The next section is devoted to the in-depth analysis of the strategies for different types of user groups, ranging from very similar groups to more diverse groups with competing preferences. Moreover, it also analyzes the strategies when varying the group size.

Evaluation
Ideally we would like to evaluate our consensus negotiation strategies through a large-scale live-user study, however, we wish to compare an array of strategies across a range of group sizes made up of members with various preference similarities. For this reason a liveuser study was unfeasible. Artificially modelling user preference information and behaviour is difficult and sometimes unreliable. In this evaluation we have endeavoured to utilise real user data in an artificial setting by combining live-user preference information and simulating the consensus negotiation of the groups.
In order to generate groups and test our consensus negotiation strategies we need user profiles made up of preference information. In this instance, we opt for a critiquing-based recommender style user profile of critique preferences [31], see Section 5.1. Critiques are directional preferences applied to a particular feature of a product, e.g. Price < $100 or Rating > 4 Stars. In this evaluation, we will use the critiquing profiles as input to the consensus negotiation strategies.

Description of the recommender
In this work, although we will describe an artificial simulation evaluation, our profiles are generated using real user data in a fashion which reflects a live user group recommender system called CATS. The Collaborative Advisory Travel System (CATS) [31], is a prototype recommender system that supports consensus decisionmaking for a group of users intending to book a skiholiday together. Very briefly, in CATS, holiday candidates are represented as product cases, each describing various features about the resort and ski-runs available. Sample product features include: package price, number of ski runs/difficulty, location, accommodation type/rating and experience level of the skier. CATS uses a common interface to share preferences among group members (see Figure 1). Importantly, a number of novel and interesting mechanisms have been put in place to maximize the amount of preference information captured from, as well as communicated to, group members (see [30][31][32]). This is so that the recommender can uncover useful information about the combined preferences of the group and make more appropriate recommendations. Group recommendation cycles start with individual group members expressing their preferences over holiday products, CATS generates individual and group recommendations by aggregating the evolving preference profiles. The recommendations are presented to the group members to allow for feedback. In this group recommender users provide feedback on holiday products using critique-based feedback [6]. The CATS system was developed to be device unspecific and prototypes were developed for multiple PCs connected over a network [31] and a table-top collaborative display [32] (see Figure 1 ).

Data and Users
For our evaluation we use a product-base of 151 European ski packages as our product cases. Each product is made up of 42 different features related to the ski resort (25 features such as country, transfer time, lift system, etc.) and the type of accommodation (17 features such as rating, price, ski room facilities, etc.). As our trialists we enlisted the help of 34 postgraduate students with a range of skiing experience. Of the participants, 7 users had skied regularly before and so were very aware of their skiing preferences, while the other 27 users were novices or first-timers with a more limited idea of their preferences (see also [31]).

Methodology
The style of this evaluation is different from others in that our test users do not participate in a live evaluation of different versions of a recommendation system as members of a set number of well-defined groups. Our goal is to evaluate group consensus negotiation recommendation across a large number of different groups with very different characteristics. Ordinarily this would mean enlisting the help of large numbers of users, which was judged to be prohibitively expensive. Therefore, instead we chose to spend significant effort eliciting the ski preferences of our test subjects and used these preferences as the basis for an off-line evaluation by combining the users into large numbers of different test groups. These test groups (and their members' preferences) are used to evaluate the recommendations made by the different group consensus negotiation strategies.

Critique-Based Profiling
In our group recommender scenario users provide feedback on holiday products (also known as cases in conversational case-based recommenders) using critiquebased feedback [5]. When presented with a recommendation the users apply contextual critiques to product features in line with their preferences. For instance, they might seek a holiday that is less/more expensive, a higher/lower standard of accommodation, or one which provides access to more/less advanced ski runs.
In order to produce these critique profiles user preferences were recorded as each test subject browsed a collection of sample ski products [31]. No recommendation techniques were used during this phase as the objective was simply to allow the user to review the available holiday options and select a single preferred product (their Final Product) in their own time. Trial subjects were also asked to complete a Web form indicating which of the Final Product features they felt positively or negatively about in order to get a clearer picture of their preferences with respect to this product. Users were also asked to design their own "Perfect Product" by completing a Web form to fill out their ideal set of ski holiday features. Users were instructed to make reasonable choices during this stage; it is unreasonable to expect a week in a 5-star hotel for $100, for example. Of course there are no guarantees that the resulting "product" will exist in the product space -in fact it is highly unlikely -but it provides us with a clear picture of each user's true preferences, broadly unconstrained by the reality of what is available. At the end of this phase, the 34 trial subjects had chosen a total of 26 unique Final Products after reviewing an average of 26 products each (i.e., the typical user chose their preferred product after viewing approximately 17% of the available products). On average each user annotated 11 features of their Final Product as positive and 3 features as negative and when they produced their Perfect Product they selected an average of 14 features.
Each of the preference profiles for the 34 trial subjects was then converted into a critique-based profile that could be used by our recommender system. To do this we inferred a set of critiques by comparing each user's Final Product features (positive and negative) to their corresponding Perfect Product features. For example, if a user indicated a positive preference for (price = $1000 ) and their corresponding Perfect Case feature for (price = $800 ) the inferred critique would be (price < $1000 ). Also for a negative preference, for example

Group Generation
From our set of 34 profiles we can generate combinatorially many groups made up of users with varying degrees of similarity. Firstly we generated groups of various sizes, and in this case our groups are made up of 3, 4, 6 and 8 individual members. We wish to see if the consensus negotiation strategies performance change with varying group size. We generated several thousand groups from our profiles and calculated the group members average similarity. To compute interuser similarity we compared users critique satisfaction with their Perfect Products. We then split these groups to form 3 sets of 100 groups. Each set of groups was made up of members with certain similarity characteristics. For example, the Similar group-set contained groups of users with a high average pairwise similarity in the range of 0.53 to 0.82. The Mixed group-set contained groups of users with a mid-range pairwise similarities in the region of 0.4. Finally, the Diverse groupset contains groups of users with average pairwise similarities from 0.04 to 0.28. Intuitively we would expect that more diverse groups will represent more challenging consensus targets as their individual members tend to have conflicting preferences.
In order to compare our consensus negotiation strategies we need a baseline. There has been little or no other published strategies for consensus negotiations for these types of group recommender systems, so a challenging baseline is difficult to locate. In this evaluation we compare our strategies against each other and the Random baseline -a product returned at random from the product space.

Consensus Negotiation
For each test group we generate consensus negotiation recommendations across all the strategies described in Section 3 and our baseline. Each simulation recommends a final list of recommendations to the group. We will evaluate consensus negotiation through the recommendation of a single top recommendation and a final recommendation list of 5 products. Typical recommender systems differ in how they display final recommendation lists with some systems preferring a single final product and others offering some choice by narrowing the options to a number of possibilities. Figure 2 shows the results for the top 1 consensus negotiation recommendation for each strategy across all of the group sizes broken down by group preference similarity. The bars represent the average similarity of the recommendation product to the Perfect Products of the group members. The graphs show similar trends for each of the group sizes allowing us to conclude that consensus negotiation is stable across different group sizes. As expected the Similar groups were easier to satisfy than the Mixed or Diverse groups. The graph shows that the Completeness, Multiplicative, Borda and Mean strategies perform best across all group sizes. LSg, Purity and Least Misery all perform admirably. Overall the best of the strategies produce a single recommendation which is between 60% and 80% similar to each members Perfect Products. All strategies outperform the Random baseline.   Figure 3 shows the percentage benefit of each strategy over the Random baseline. Again, as expected, the Similar groups receive the greatest share of the benefit. Interestingly however, as the group size gets larger the more Diverse groups receive a greater benefit, with Multiplicative and Completeness offering the most for the most diverse 8 member groups.
In Figure 4 we examine the results when the top 5 consensus negotiation recommendations are offered to the group. The bars in these graphs represent the average similarity of the top 5 recommendations to the Perfect Products of the group members. The results for the top 5 recommendations are broadly similar to those produced in the single recommendation analysis with Multiplicative, Borda Count and Completeness performing best, closely followed by Purity, Least Misery and LSg. Again, the strategies are stable across various group sizes and various inter-member similarities and all outperform the Random baseline. Once again, the result trends are similar when we look at the percentage benefit of the strategies over the Random baseline ( Figure 5). So not only are the results stable across differing inter-member similarity of various size groups for a single top 1 consensus recommendation, but they are also stable and offer similar benefits when a list of top 5 consensus products are recommended.

Statistical analysis
We also statistically analyze the benefits of using each one of the strategies. First of all, we compute the mean rank (r) of each strategy considering all the experiments (three different types of groups with four group sizes). The rankings are obtained estimating each particular ranking r j i for each experiment i and each strategy j, and computing the mean ranking R for each strategy as R j = 1 N i r j i , where N is the total number of experiments. Compared with mean performance val-  ues, the mean rank reduces the susceptibility to outliers which, for instance, allows a classifier's excellent performance in one experiment to compensate for its overall bad performance [10]. Secondly, we apply the Friedman and Nemenyi tests to analyze whether the difference between algorithms is statistically significant [13,14].
The Friedman test, recommended by Demšar [10], is effective for comparing multiple strategies or algorithms across multiple data sets (in our case, across multiple experiments). It compares the mean ranks of strategies to decide whether to reject the null hypothesis, which states that all the methods are equivalent and therefore their ranks should be equal. The Friedman statistic value is computed as follows: where k is the number of strategies to compare.
Since this value is undesirably conservative, Iman and Davenport [18] proposed a corrected statistic: When we apply the Friedman test in our experiments with ten strategies and twelve different experiments, F F is distributed according to the F distribution with (10 − 1) = 9 and (10 − 1) · (12 − 1) = 99 degrees of freedom. The critical value of F(9,99) = 2,59 at the 0,01 critical level. For our experiments on the Ski dataset we obtained the values of X F = 97, 65 and F F = 103, 78 and, X F = 95, 57 and F F = 84, 60 for the Top 1 and Top 5 experiments, respectively. As the values are higher than 2,59 we can reject the null hypothesis in both cases.
Once we have checked for the non-randomness of the results, we can perform a post hoc test to check if one of the techniques can be singled out. For this purpose, we use the Nemenyi test -two techniques are significantly different if the corresponding average ranks differ by at least the critical difference value: where q α is based on the Studentized range statistic divided by √ 2 and k is the number of algorithms to compare. In our case, when comparing ten strategies with a critical value α = 0.05, q 0.05 = 3.164 for a twotailed Nemenyi test. Substituting, we obtain a critical difference value CD = 3.91. Thus, for any two pairs of algorithms whose rank difference is higher than 3.91, we can infer -with a confidence of 95%-that there exists a significant difference between them.
For the top 1 product recommendation, the results of the Nemenyi test are illustrated in Figure 6. In the figure, diamonds represent the mean ranks of each strategy. Vertical lines across diamonds indicate the 'critical difference'. The performance of two strategies is significantly different if their corresponding mean ranks differ by at least the critical difference. For instance, Figure 6 reveals that Completeness is significantly better than Purity. However, we cannot say the same with regard to Mean or LS g , though. Note that the best mean rank corresponds to Multiplicative strategy, closely followed by Completeness and Borda. Random strategy obtains the worst mean rank, as expected. Multiplicative, Completeness and Borda performance are significantly better than Purity, GSg, Most Pleasure and Random strategies.
A similar behavior occurs with the top 5 analysis of Figure 7. However, in this case, the best mean rank corresponds to the Completeness strategy, closely followed by the Multiplicative and Borda.
In summary, our statistical significance analysis has shown that Multiplicative, Completeness and the Borda strategies work particularly well across different group sizes and different types of users, as the three strategies present the lowest mean rank. Moreover, the results also show that these strategies are significantly better than Purity, GS g , Most Pleasure and random strategies. On the other hand, it is interesting to note that Average, LS g and Least misery present a greater mean rank than Completeness, Multiplicative and Borda although they are not significant differences among them. We can conclude that these strategies are well suited for consensus as they are stable across different combinations of users.

Conclusions
In this paper, we have introduced the little considered problem of consensus negotiation in group recommender systems. These systems differ from normal personalization recommenders as they aim to recommend personalized products to a group of users. These groups can be of various sizes and can be composed of members who may have conflicting product preferences. All of these possible variances make for an interesting research challenge. Here we have introduced nine consensus negotiation strategies to help the personalization process at the end of a session in a group scenario. The consensus negotiation strategies introduced are based on statistical, content and collaborative ideas. We carried out a large artificial simulation using real user preference information based on a ski holiday group recommender system employing critique-based feedback. The results are positive, with some significance, and the strategy behaviors are consistent across various group size and inter-member similarity. To date the issue of consensus negotiation has remained an acknowledged but unresolved challenge in this area of personalization. This work represents the first step in tackling this area of research.
As a matter of future work we would like to try and perform a deeper analysis of the behaviors of group consensus negotiation strategies. Although a full scale live-user study may still be premature, we wish to con-tinue to develop our off line simulator and our ability to capture real user preference profiles for the purposes of introducing and testing new group recommendation ideas.


extfieldsofstudy:
Computer Science
Physics
Mathematics

text:
Open Bisimulation for Quantum Processes

Quantum processes describe concurrent communicating systems that may involve quantum information. We propose a notion of open bisimulation for quantum processes and show that it provides both a sound and complete proof methodology for a natural extensional behavioural equivalence between quantum processes. We also give a modal characterisation of open bisimulation, by extending the Hennessy-Milner logic to a quantum setting.

Introduction
The theory of quantum computing has attracted considerable research efforts in the past twenty years. Benefiting from the superposition of quantum states and linearity of quantum operations, quantum computing may provide considerable speedup over its classical analogue [39,14,15]. However, functional quantum computers which can harness this potential in dealing with practical applications are extremely difficult to implement. On the other hand, quantum cryptography, of which the security and ability to detect the presence of eavesdropping are provable based on the principles of quantum mechanics, has been developed so rapidly that quantum cryptographic systems are already commercially available by a number of companies such as Id Quantique, Cerberis, MagiQ Technologies, SmartQuantum, and NEC.
As is well known, it is very difficult to guarantee the correctness of classical communication protocols at the design stage, and some simple protocols were finally found to have fundamental flaws. Since human intuition is poorly adapted to the quantum world, quantum protocol designers will definitely make more faults than classical protocol designers, especially when more and more complicated quantum protocols can be implemented by future physical technology. In view of the success that classical process algebras [28,19,1] achieved in analyzing and verifying classical communication protocols, several research groups proposed various quantum process algebras with the purpose of modeling quantum protocols. Jorrand and Lalire [25,27] defined a language QPAlg (Quantum Process Algebra) by adding primitives expressing unitary transformations and quantum measurements, as well as communications of quantum states, to a CCS-like classical process algebra. An operational semantics of QPAlg is given, and further a probabilistic branching bisimulation between quantum processes is defined. Gay and Nagarajan [12,13] proposed a language CQP (Communicating Quantum Processes), which is obtained from the pi-calculus [29] by adding primitives for measurements and transformations of quantum states, and allowing transmission of qubits. They presented a type system for CQP, and in particular proved that the semantics preserves typing and that typing guarantees that each qubit is owned by a unique process within a system. The second author of the current paper, together with his colleagues, proposed a language named qCCS [9,41,10] for quantum communicating systems by adding quantum input/output and quantum operation/measurement primitives to classical value-passing CCS [16,17]. One distinctive feature of qCCS, compared to QPAlg and CQP, is that it provides a framework to describe, as well as reason about, the communication of quantum systems which are entangled with other systems. Furthermore, a bisimulation for processes in qCCS has been introduced, and the associated bisimilarity is proven to be a congruence with respect to all process constructors of qCCS.
Uniqueness of the solutions to recursive process equations is also established, which provides a powerful proof technique for verifying complex quantum protocols.
In the study of quantum systems, as well as classical communicating systems, an important problem is to tell if two given systems exhibit the same behaviour. To approach the problem we first need to give criteria for reasonable behavioural equivalence. Two systems should only be distinguished on the basis of the chosen criteria. Therefore, these criteria induce an extensional equivalence between systems, ≈ behav , namely the largest equivalence which satisfies them.
Having an independent notion of which systems should, and which should not, be distinguished, one can then justify a particular notion of equivalence, e.g. bisimulation, by showing that it captures precisely the touchstone equivalence. In other words, a particular definition of bisimulation is appropriate because ≈ bisi , the associated bisimulation equivalence, (i) is sound with respect to the touchstone equivalence, that is s 1 ≈ bis s 2 implies s 1 ≈ behav s 2 ; (ii) provides a complete proof methodology for the touchstone equivalence, that is s 1 ≈ behav s 2 implies s 1 ≈ bis s 2 .
This approach originated in [20] but has now been widely used for different process description languages; for example, see [21,34] for its application to higher-order process languages, [32] for mobile ambients, [11] for asynchronous languages and [5] for probabilistic timed languages. Moreover, in each case the distinguishing criteria are more or less the same. The touchstone equivalence should (i) be compositional ; that is preserved by some natural operators for constructing systems; (ii) preserve barbs; barbs are simple experiments which observers may perform on systems [33]; (iii) be reduction-closed ; this is a natural condition on the reduction semantics of systems which ensures that nondeterministic choices are in some sense preserved.
We adapt this approach to quantum processes. Using natural versions of these criteria we obtain an appropriate touchstone equivalence, which we call reduction barbed congruence, ≈ r . We then develop a theory of bisimulations which is both sound and complete for ≈ r . Moreover, we provide a modal characterisation of ≈ r in a quantum logic based on Hennessy-Milner logic [18]by establishing the coincidence of the largest bisimilation with logical equivalence.
The remainder of the paper is organised as follows. In the next section we recall some preliminary concepts from quantum theory. In Section 3 we review the model of probabilistic labelled transition systems, based on which we give the operational semantics of qCCS in Section 4. Section 5 contains the main theoretical results of the paper. We define a notion of open bisimulation, which is shown to be a congruence relation in the language of qCCS. It turns out that open bisimilarity precisely captures reduction barbed congruence, thus provides a sound and complete proof methodology for our touchstone equivalence. In addition, we give a modal characterisation of the equivalence in a quantum logic obtained by an extension of Hennessy-Milner logic with a probabilistic choice modality and a super-operator application modality. To illustrate the application of open bisimulation and its modal characterisation, in Section 6 we describe the key distribution protocol BB84 as qCCS processes and compare a specification with its implementations of the protocol. The paper ends with a brief comparison with related work in Section 7.

Preliminaries on quantum mechanics
In this section, we briefly recall some basic concepts from quantum theory, which requires first some notions from linear algebra. More details about quantum computation can be found in many books, e.g. [30].

Basic linear algebra
A Hilbert space H is a complete vector space equipped with an inner product ·|· : H × H → C such that 1. ψ|ψ ≥ 0 for any |ψ ∈ H, with equality if and only if |ψ = 0; where C is the set of complex numbers, and for each c ∈ C, c * stands for the complex conjugate of c. For any vector |ψ ∈ H, its length |||ψ || is defined to be ψ|ψ , and it is said to be normalized if |||ψ || = 1. Two vectors |ψ and |φ are orthogonal if ψ|φ = 0. An orthonormal basis of a Hilbert space H is a basis {|i } where each |i is normalized and any pair of them are orthogonal.
Let L(H) be the set of linear operators on H. For any A ∈ L(H), A is Hermitian if A † = A where A † is the adjoint operator of A such that ψ|A † |φ = φ|A|ψ * for any |ψ , |φ ∈ H. The fundamental spectral theorem [30] states that the set of all normalized eigenvectors of a Hermitian operator in L(H) constitutes an orthonormal basis for H. That is, there exists a so-called spectral decomposition for each Hermitian A such that where the set {|i } constitutes an orthonormal basis of H, spec(A) denotes the set of eigenvalues of A, and E i is the projector to the corresponding eigenspace of where I H is the identity operator on H. For instance, a well-known unitary operator is the 1-qubit Hadamard operator H defined as follows: The trace of A ∈ L(H) is defined as tr(A) = i i|A|i for some given orthonormal basis {|i } of H. It is worth noting that trace function is actually independent of the chosen orthonormal basis. It is also easy to check that trace function is linear and tr(AB) = tr(BA) for any operators A, B ∈ L(H).
Let H 1 and H 2 be two Hilbert spaces. Their tensor product H 1 ⊗H 2 is defined as a vector space consisting of linear combinations of the vectors |ψ 1 ψ 2 = |ψ 1 |ψ 2 = |ψ 1 ⊗ |ψ 2 with |ψ 1 ∈ H 1 and |ψ 2 ∈ H 2 . Here the tensor product of two vectors is defined by a new vector such that Then H 1 ⊗ H 2 is also a Hilbert space where the inner product is defined as the following: for any |ψ 1 , |φ 1 ∈ H 1 and |ψ 2 , where ·|· Hi is the inner product of H i . For any A 1 ∈ L(H 1 ) and A 2 ∈ L(H 2 ), A 1 ⊗ A 2 is defined as a linear operator in L(H 1 ⊗ H 2 ) such that for each |ψ 1 ∈ H 1 and |ψ 2 ∈ H 2 , The partial trace of A ∈ L(H 1 ⊗ H 2 ) with respected to H 1 is defined as tr H1 (A) = i i|A|i where {|i } is an orthonormal basis of H 1 . Similarly, we can define the partial trace of A with respected to H 2 . Partial trace functions are also independent of the orthonormal basis selected.
An operator A ∈ L(H) is positive if ψ|Aψ ≥ 0 for every ψ ∈ H. A linear operator E on L(H) is completely positive if it maps positive operators in L(H) to positive operators in L(H), and for any auxiliary Hilbert space H ′ , the trivially extended operator I H ′ ⊗ E also maps positive operators in L(H ′ ⊗ H) to positive operators in L(H ′ ⊗ H). Here I H ′ is the identity operator on L(H ′ ). The elegant and powerful Kraus representation theorem [26] of completely positive operators states that a linear operator E is completely positive if and only if there is some set of operators {E i } with appropriate dimension such that The operators E i are called Kraus operators of E. A linear operator is said to be a super-operator if it is completely positive and trace-nonincreasing. Here an operator E is trace-nonincreasing if tr(E(A)) ≤ tr(A) for any positive A ∈ L(H), and it is said to be trace-preserving if the equality always holds. Then a super-operator (resp. a trace-preserving super-operator) is a completely positive operator with its Kraus operators We denote by SO(H) the set of trace-preserving super-operators on the Hilbert space H.

Basic quantum mechanics
According to von Neumann's formalism of quantum mechanics [40], an isolated physical system is associated with a Hilbert space which is called the state space of the system. A pure state of a quantum system is a normalized vector in its state space, and a mixed state is represented by a density operator on the state space. Here a density operator ρ on Hilbert space H is a positive linear operator such that tr(ρ) = 1. Another equivalent representation of density operator is probabilistic ensemble of pure states. In particular, given an ensemble {(p i , |ψ i )} where p i ≥ 0, i p i = 1, and |ψ i are pure states, then ρ = i p i [|ψ i ] is a density operator. Here [|ψ i ] denotes the abbreviation of |ψ i ψ i |. Conversely, each density operator can be generated by an ensemble of pure states in this way. The set of density operators on H can be defined as The state space of a composite system (for example, a quantum system consisting of many qubits) is the tensor product of the state spaces of its components. For a mixed state ρ on H 1 ⊗ H 2 , partial traces of ρ have explicit physical meanings: the density operators tr H1 ρ and tr H2 ρ are exactly the reduced quantum states of ρ on the second and the first component system, respectively. Note that in general, the state of a composite system cannot be decomposed into tensor product of the reduced states on its component systems. A well-known example is the 2-qubit state This kind of state is called entangled state. To see the strangeness of entanglement, suppose a measurement is applied on the first qubit of |Ψ (see the following for the definition of quantum measurements). Then after the measurement, the second qubit will definitely collapse into state |0 or |1 depending on whether the outcome λ 0 or λ 1 is observed. In other words, the measurement on the first qubit changes the state of the second qubit in some way. This is an outstanding feature of quantum mechanics which has no counterpart in classical world, and is the key to many quantum information processing tasks such as teleportation [3] and superdense coding [4]. The evolution of a closed quantum system is described by a unitary operator on its state space: if the states of the system at times t 1 and t 2 are ρ 1 and ρ 2 , respectively, then ρ 2 = U ρ 1 U † for some unitary operator U which depends only on t 1 and t 2 . In contrast, the general dynamics which can occur in a physical system is described by a trace-preserving super-operator on its state space. Note that the unitary transformation U (ρ) = U ρU † is a trace-preserving super-operator.
A quantum measurement is described by a collection {M m } of measurement operators, where the indices m refer to the measurement outcomes. It is required that the measurement operators satisfy the completeness (1) its spectral decomposition. We call M non-degenerate if for any m ∈ spec(M ), the corresponding projector E m is 1-dimensional; that is, all eigenvalues of M are nondegenerate. Non-degenerate measurement is obviously a very special case of general quantum measurement. However, when an ancilla system lying at a fixed state is provided, non-degenerate measurements together with unitary operators are sufficient to implement general measurements [30].

A probabilistic model
In this section we review the model of probabilistic labelled transition systems (pLTSs), and some properties of weak transitions. Later on we will interpret the behaviour of quantum processes in terms of pLTSs.

Probabilistic labelled transition systems
We begin with some notation. A (discrete) probability distribution over a set S is a function ∆ : S → [0, 1] with s∈S ∆(s) = 1; the support of such a ∆ is the set ⌈∆⌉ = { s ∈ S | ∆(s) > 0 }. The point distribution s assigns probability 1 to s and 0 to all other elements of S, so that ⌈s⌉ = s. We use D(S) to denote the set of distributions over S, ranged over by ∆, Θ etc. If k∈K p k = 1 for some collection of p k ≥ 0, and the ∆ k are distributions, then so is k∈K p k · ∆ k with ( k∈K p k · ∆ k )(s) = i∈I p i · ∆ i (s). (ii) Act τ is a set of transition labels, with distinguished element τ ; In the literature essentially the same model has appeared under different names such as NP-systems [22], probabilistic processes [23], simple probabilistic automata [37], probabilistic transition systems [24] etc. Furthermore, there are strong structural similarities with Markov Decision Processes [31,8].
A (non-probabilistic) labelled transition system (LTS) may be viewed as a degenerate pLTS, one in which only point distributions are used.

Lifting relations
In a pLTS actions are only performed by states, in that actions are given by relations from states to distributions. But in general we allow distributions over states to perform an action. For this purpose, we lift these relations so that they also apply to distributions [7].
There are numerous ways of formulating this concept of lifting relations. The following is particularly useful.
• If ∆ R † Θ because of ∆ = s and s R Θ, then we can simply take I to be the singleton set {i} with p i = 1 and Θ i = Θ.
• If ∆ R † Θ because of the conditions ∆ = i∈I p i · ∆ i , Θ i = i∈I p i · Θ i for some index set I, and ∆ i R † Θ i for each i ∈ I, then by induction hypothesis there are index sets J i such that ∆ i = j∈Ji p ij · s ij , Θ i = j∈Ji p ij · Θ ij , and s ij R Θ ij for each i ∈ I and j ∈ J i . It follows that ∆ = i∈I j∈Ji p i p ij · s ij , Θ = i∈I j∈Ji p i p ij · Θ ij , and s ij R Θ ij for each i ∈ I and j ∈ J i . So it suffices to take {ij | i ∈ I, j ∈ J i } to be the index set and {p i p ij | i ∈ I, j ∈ J i } be the collection of probabilities.
We apply this operation to the relations α −→ in the pLTS for α ∈ Act τ , where we also write Thus as source of a relation α −→ we now also allow distributions. But note that s α −→ ∆ is more general than s α −→ ∆. In papers such as [38,6] the former is refered to as a combined transition because if s α −→ ∆ then there is a collection of distributions ∆ i and probabilities p i such that s α −→ ∆ i for each i ∈ I and ∆ = i∈I p i · ∆ i with i∈I p i = 1.
In Definition 3.2, linearity tells us how to compare two linear combinations of distributions. Sometimes we need a dual notion of decomposition. Intuitively, if a relation R is left-decomposable and ∆ R Θ, then for any decomposition of ∆ there exists some corresponding decomposition of Θ. Proof. Suppose ∆ = ( i∈I p i · ∆ i ) and ∆ R † Θ. We have to find a family of Θ i such that From the alternative characterisation of lifting, Lemma 3.3, we know that Note that ∆(s) can be written as { j∈J | s=sj } q j and therefore For any a ∈ Act τ , we know thatâ −→ ⊆ S × D(S), so we can lift it to be a transition relation between distributions. With a slight abuse of notation we simply write ∆â −→ Θ for ∆ (â −→) † Θ. Then we define weak transitionsâ =⇒ by lettingτ =⇒ be the reflexive and transitive closure ofτ −→ and writing ∆â =⇒ Θ for a ∈ Act whenever ∆τ =⇒â −→τ =⇒ Θ. If ∆ is a point distribution, we often write sâ =⇒ Θ instead of sâ =⇒ Θ. Proof. It is easy to check that both properties are preserved by composition; that is if R i , i = 1, 2, are linear, left-decomposable respectively, then so is R 1 · R 2 . The result now follows sinceα =⇒ is formed by repeated composition from two relationsτ −→ andα −→ which we know are both linear and left-decomposable.
Let R ⊆ S × S be a relation between states. It induces a speical relationR ⊆ S × D(S) between states and distributions:R Then we can use Definition 3.2 to liftR to be a relation (R) † between distributions. For simplicity, we combine the above two lifting operations and directly write R † for (R) † in the sequel, with the intention that a relation between states can be lifted to a relation between distributions via a special application of Definition 3.2. Consequently, we have the following corollary of Lemma 3.3.
Relations over distributions obtained by lifting enjoy some very useful properties. The following one will be used in Section 5 to show the transitivity of open bisimilarity.
Then we have that The middle part of (2) implies the existence of some states t i such that Then we show the inverse inclusion Then from ∆ 2 R 2 † ∆ 3 and Proposition 3.5, we have Finally, it follows from (4) and the fact

Quantum CCS
We introduce the language qCCS which was originally studied in [9,41,10]. Three types of data are considered in qCCS: as classical data we have Bool for booleans and Real for real numbers, and as quantum data we have Qbt for qubits. Consequently, two countably infinite sets of variables are assumed: cV ar for classical variables, ranged over by x, y, ..., and qV ar for quantum variables, ranged over by q, r, .... We assume a set Exp, which includes cV ar as a subset and is ranged over by e, e ′ , . . . , of classical data expressions over Real, and a set of boolean-valued expressions BExp, ranged over by b, b ′ , . . . , with the usual boolean constants true, false, and operators ¬, ∧, ∨, and →. In particular, we let e ⊲⊳ e ′ be a boolean expression for any e, e ′ ∈ Exp and ⊲⊳∈ {>, <, ≥, ≤, =}. We further assume that only classical variables can occur free in both data expressions and boolean expressions. Two types of channels are used: cChan for classical channels, ranged over by c, d, ..., and qChan for quantum channels, ranged over by c,d,.... A relabelling function f is a map on cChan ∪ qChan such that f (cChan) ⊆ cChan and f (qChan) ⊆ qChan. Sometimes we abbreviate a sequence of distinct variables q 1 , ..., q n intoq. The terms in qCCS are given by: where f is a relabelling function and L ⊆ cChan ∪ qChan is a set of channels. Most of the constructors are standard as in CCS [28]. We briefly explain a few new constructors. The process c?q.P receives a quantum datum along quantum channel c and evolves into P . The process c!q.P sends out a quantum datum along quantum channel c before evolving into P . The new symbols E and M represent respectively a trace-preserving super-operator and a non-degenerate projective measurement applying on the Hilbert space associated with the systemsq. Free classical variables can be defined in the usual way, except for the fact that the variable x in the The set of free quantum variables for process P , denoted by qv(P ) can be inductively defined as follows.
For a process to be legal, we require that 1. q ∈ qv(P ) in the process c!q.P ; 2. qv(P ) ∩ qv(Q) = ∅ in the process P || Q; 3. Each constant A(q;x) has a defining equation A(q;x) := P , where P is a term with qv(P ) ⊆q and f v(P ) ⊆x.
The first condition says that a quantum system will not be referenced after it has been sent out. This is a requirement of quantum no-cloning theorem. The second condition says that parallel composition || models separate parties that never reference a quantum system simultaneously. Throughout the paper we implicitly assume the convention that processes are identified up to α-conversion, bound variables differ from each other and they are different from free variables.
We now turn to the operational semantics of qCCS. For each quantum variable q we assume a 2dimensional Hilbert space H q . For any nonempty subset S ⊆ qV ar we write H S for the tensor product space q∈S H q . In particular, H = H qVar is the state space of the whole environment consisting of all the quantum variables, which is a countably infinite dimensional Hilbert space.
Let P be a closed quantum process and ρ a density operator on H, the pair P, ρ is called a configuration. We write Con for the set of all configurations, ranged over by C and D. We interpret qCCS as a pLTS whose states are all the configurations definable in the language, and whose arrows are determined by the rules in Figure 1; we have omitted the obvious symmetric counterparts to the rules (C-Com), (Q-Com), (Int) and (Sum). The set of actions Act takes the form The symbol τ denotes invisible actions. We write Act τ for Act ∪ {τ }, which is ranged over by α. We use cn(α) for the set of channel names in action α. So, for example, cn(c?x) = {c} and cn(τ ) = ∅.
In the first eight rules in Figure 1, the targets of arrows are point distributions, and we use the slightly abbreviated form C α −→ C ′ to mean C α −→ C ′ . The rules use the obvious extension of the function || on terms to configurations and distributions. To be precise, C || P is the configuration Q || P, ρ where C = Q, ρ , and ∆ || P is the distribution defined by: Similar extension applies to ∆[f ] and ∆\L.

Open bisimulations
Let C = P, ρ . We use the notation qv (C) := qv(P ) for free quantum variables and ptr(C) := tr qv(P ) (ρ) for partial traces. Let ∆ = i∈I p i · P i , ρ i . We write E(∆) for the distribution i∈I p i · P i , E(ρ i ) . • whenever E(C) The above definition is inspired by the work of Sangiorgi [36], where a notion of bisimulation is defined for the π-calculus by treating name instantiation in an "open" style. Here we deal with super-operator application in an "open" style, but the instantiation of variables is in an "early" style because the operational semantics given in Figure 1 is essentially an early semantics. For more variants of semantics, see e.g. [35].
In this paper we are mainly interested in a notion of weak open bisimulation which is like strong open bisimulation but internal transitions are abstracted away. Two quantum processes P and Q are bisimilar, denoted by P ≈ o Q, if for any quantum state ρ ∈ D(H) and any indexed setṽ of classical values, we have Herex is the set of free classical variables contained in P and Q.

A useful proof technique
In Definition 5.2 super-operator application and transitions are considered at the same time. In fact, we can separate the two issues and approach the concept of open bisimulation in an incremental way, which turns out to be very useful when proving that two configurations are open bisimilar.

Definition 5.3. A relation R⊆ Con × Con is closed under super-operator application if C R D implies E(C) R E(D) for any E ∈ SO(H qv(C) ).
Definition 5.4. A relation R⊆ Con × Con is a ground simulation if C R D implies that qv (C) = qv (D), ptr(C) = ptr(D), and A relation R is a ground bisimulation if both R and R −1 are ground simulations. Proof. Suppose that C R D. Since R is a ground bisimulation, we have qv (C) = qv (D) and ptr(C) = ptr(D). Since R is closed under all super-operator application, we have E(C) R E(D) for any E ∈ SO(H qv(C) ). If E(C) α −→ ∆, then there exists some distribution Θ such that E(D)α =⇒ Θ and ∆ R † Θ because R is a ground bisimulation. Similarly, any transtion from E(D) can also be matched up by E(C). Therefore, R is an open bisimulation.
The above proposition provides us a useful proof technique: in order to show that two configurations C and D are open bisimilar, it sufficies to exhibit a binary relation including the pair (C, D), and then to check that the relation is a ground bisimulation and is closed under all super-operator application. This is analogous to a proof technique of open bisimulation for the π-calculus [36], where name instantiation is playing the same role as super-operator application here.
Proposition 5.6. ≈ o is the largest ground bisimulation that is closed under all super-operator application.
Proof. By definition ≈ o is closed under all super-operator application. It is is obviously a ground bisimulation. Moreover, it is the largest one because of Proposition 5.5.

Equivalence and congruence
As a sanity check, we prove that ≈ o is an equivalence relation. This is based on the following transfer property.
Proof. Suppose ∆ ≈ o † Θ and ∆ α −→ ∆ ′ . By Corollary 3.7, there is a finite index set I such that (i) ∆ = i∈I p i · C i , (ii) Θ = i∈I p i · D i , and (iii) C i ≈ o D i for each i ∈ I. By the condition ∆ α −→ ∆ ′ , (i) and Proposition 3.5, we can decompose ∆ ′ into i∈I p Sinceα =⇒ is linear by Proposition 3.6, we know that Θ = i∈I p i j∈Ji q ij D iα =⇒ Θ ′ . By the linearity of The result now follows from the transitivity ofτ =⇒.
Theorem 5.9. ≈ o is an equivalence relation.
Proof. It is trivial to see that ≈ o is reflexive and symmetric. For transitivity, we show that ≈ o · ≈ o is an open bisimulation relation. Since this is a symmetric relation, we only need to show that it is an open simulation.
As a relation between configurations, ≈ o is preserved by all static constructors.
Proof. We only prove (1) as an example. Let It suffices to show that R is an open bisimulation. Suppose P R, ρ R Q R, σ where P, ρ ≈ o Q, σ . By the definition of ≈ o we have that qv(P ) = qv(Q) and tr qv(P ) (ρ) = tr qv(Q) (σ). Thus qv(P R) = qv(Q R) and we infer that tr qv(P R) (ρ) = tr qv(P R)\qv(P ) tr qv(P ) (ρ) = tr qv(Q R)\qv(Q) tr qv(Q) (σ) = tr qv(Q R) (σ). By Proposition 5.6, we know that P, E(ρ) ≈ o Q, E(σ) for any E ∈ SO(H qv(P ) ), from which it follows that P || R, E(ρ) R Q || R, E(σ) for any E ∈ SO(H qv(P ||R) ). In other words, R is closed under super-operator application. Below we show that it is also a ground bisimulation.
Suppose P R, ρ α −→ ∆ for some α and ∆. There are three cases to consider.

The transition is caused by
Furthermore, by Proposition 5.6, we have P, E i (ρ) ≈ o Q, E i (σ) , and then ∆ R † Θ by definition.
2. The transition is caused by P solely; that is, P, ρ 3. The transition is caused by a communication between P and R. Without loss of generality, we assume that P, ρ and ∆ = P ′ R ′ , ρ . By a simple induction on the rules in Figure 1, it is easy to see that R, η c!q −→ R ′ , η for any η ∈ D(H).

From the assumption that
such that for any i ∈ I, it holds that P ′ , ρ ≈ o Q i , σ i and Furthermore, for any i ∈ I, we have The symmetric form when Q R, E(σ) α −→ Θ can be similarly proved. So R is a ground bisimulation on Con. It follows from Proposition 5.5 that R is also an open bisimulation.
Note that we do not have a counterpart of the above proposition for dynamic constructors such as prefix. As a counterexample, consider the following two configurations taken from [10]: Theorem 5.11. The relation ≈ o between processes is preserved by all the constructors of qCCS except for summation.
Proof. Similar to the proof of Theorem 6.17 in [10], which shows the congruence property of a notion of weak bisimulation.

An extensional equivalence
We formally define three criteria, namely barb-preservation, reduction-closedness and composionality, in order to judge whether two processes are equivalent. This yields an extensional equivalence that turns out to coincide with open bisimilarity.
for any classical channel c; whenever Dτ =⇒ Θ, there exists ∆ such that Cτ =⇒ ∆ and ∆ R † Θ; • compositional if C R D implies (C||R) R (D||R) for any process R with qv(R) disjoint from qv(C) ∪ qv(D), and R is closed under super-operator application.
Definition 5.14 (Reduction barbed congruence). Let reduction barbed congruence, denoted by ≈ r , be the largest relation over configurations which is barb-preserving, reduction-closed and compositional, and furthermore, if C ≈ r D then qv (C) = qv (D) and ptr(C) = ptr(D).
Proof. By Corollary 5.8 and Proposition 5.10 we know that ≈ o is reduction closed and compositional. It remains to show that ≈ o is barb-preserving. Suppose C ≈ o D and C ⇓ ≥p c , for any classical channel c and probability p; we need to show that D ⇓ ≥p c . We see from C ⇓ ≥p c that Cτ =⇒ ∆ for some ∆ with V c (∆) ≥ p. By Corollary 5.8, the relation ≈ o is reductionclosed. Hence, there exists Θ such that Dτ =⇒ Θ and ∆ ≈ o † Θ. The latter means that By the second part of (5), if C i −→ for some v}, and Θ ′ be the distribution By the linearity and reflexivity ofτ =⇒, Proposition 3.6, we have Θτ =⇒ Θ ′ . It follows from Dτ =⇒ Θτ =⇒ Θ ′ that Dτ =⇒ Θ ′ . It remains to show that V c (Θ ′ ) ≥ p.
Note that for each i ∈ I c we have Θ i In order to obtain completeness, the converse of Theorem 5.15, we make use of a proof technique that involves examing the barbs of processes in certain contexts; the following technical lemma enhances this technique.
Below we check that R is compositional, barb-preserving and reduction-closed.
1. R is compositional. For any process R with qv(R) disjoint from qv(C) and c fresh for R, since ≈ r is compositional, we have (C||c!0||R) ≈ r (D||c!0||R), which means (C||R) R (D||R). By the compositionality of ≈ r we also have E(C || c!0) ≈ r E(D || c!0) for any E ∈ SO(H qv(C||c!0) ). Since qv(C) = qv(C || c!0), we have E ∈ SO(H qv(C) ). Note that It follows that E(C) R E(D) and thus R is closed under super-operator application.
2. R is barb-preserving. Suppose C ⇓ ≥p c1 for some channel c 1 and probability p. Let c 2 be some fresh channel. We construct the process T by letting T = c 1 ?x 1 .c?x.c 2 !0 for any x 1 and x. Since ≈ r is compositional, we have (C || c!0 || T ) ≈ r (D || c!0 || T ). Note that (C || c!0 || T ) ⇓ ≥p c2 , which implies (D || c!0 || T ) ⇓ ≥p c2 . Since c is fresh for D, the latter has no potential to communicate at channel c. Therefore, it must be the case that D ⇓ ≥p c1 .
Proof. Since ≈ r is closed under any super-operator application, by Proposition 5.5 it suffices to show that ≈ r is a ground bisimulation. By the symmetry of ≈ r , we only need to show that ≈ r is a ground simulation. Suppose C = P, ρ , D = Q, σ and C ≈ r D. By definition, we have qv (P ) = qv (Q) and tr qv (P ) (ρ) = tr qv(Q) (σ). Suppose C α −→ ∆. We distinguish several cases.

α ≡ c!v. Let T be the process defined by
where α ∈ Act τ , E is a super-operator, and E is a projector associated with a certain subspace of H q . We call φ a configuration formula and ψ a distribution formula. Note that a distribution formula ψ only appears as the continuation of a diamond modality α ψ.
• C |= ¬φ if it is not the case that C |= φ.
With a slight abuse of notation, we write ∆ |= ψ above to mean that ∆ satisfies the distribution formula ψ. A logical equivalence arises from the logic naturally: It turns out that L is adequate with respect to open bisimilarity. Proof.
Since ≈ o is symmetric, it suffices to prove that C |= φ implies D |= φ by structural induction on φ.
It follows that D |= E ≥p q . • Let C |= i∈I φ i . Then C |= φ i for each i ∈ I. So by induction D |= φ i , and we have D |= i∈I φ i .
• Let C |= α i∈I p i · φ i . Then Cα =⇒ ∆ and ∆ |= i∈I p i · φ i for some ∆. So ∆ = i∈i p i · ∆ i and for all i ∈ I and C ′ ∈ ⌈∆ i ⌉ we have C ′ |= φ i . Since C ≈ o D, by Corollary 5.8 there is some Θ with Dα =⇒ Θ and ∆ ≈ o † Θ. Since the lifted relation is left-decomposable, we have that Θ = i∈I p i · Θ i and ∆ Proposition 5.6 and qv(C) = qv(D). By induction, we have E(D) |= φ. It follows that D |= E.φ.
Next, we show that the relation = L is a ground bisimulation. Suppose C = L D and C α −→ ∆. We have to show that there is some Θ with Dα =⇒ Θ and ∆ (= L ) † Θ. Consider the set For each Θ ∈ T , there must be some C ′ Θ ∈ ⌈∆⌉ and D ′ In the latter case we set φ Θ = ¬φ ′ Θ and return back to the former case. So for each C ′ ∈ ⌈∆⌉ it holds that It is clear that C |= φ, hence D |= φ by C = L D. It follows that there must be a Θ * with Dα =⇒ Θ * , This means that Θ * ∈ T and hence for each C ′ ∈ ⌈∆⌉, D ′ ∈ ⌈Θ * C ′ ⌉ we have C ′ = L D ′ . It follows that ∆ (= L ) † Θ * . By symmetry all transitions of D can be matched up by transitions of C.
Finally, we prove that the relation = L is closed under super-operator application. That is, for any E ∈ SO(H qv(C) ) we need to show that C = L D implies E(C) = L E(D). Suppose C = L D and let φ be any formula such that E(C) |= φ. We have C |= E.φ. It follows from C = L D that qv(C) = qv (D) and D |= E.φ. Therefore, we obtain E(D) |= φ. By symmetry if φ is satisfied by E(D) then it is also satisfied by E(C). In other words, we have E(C) = L E(D). Now by appealing to Proposition 5.5 we see that = L is an open bisimulation, thus = L ⊆ ≈ o .
Note that the set T in (7) is infinite in general as D may have infinitely many different derivatives, hence we have to use infinite conjunction in (8). This is the reason that we cannot restrict ourselves to finite or binary conjunction in Definition 5.18.

Examples
BB84, the first quantum key distribution protocol developed by Bennett and Brassard in 1984 [2], provides a provably secure way to create a private key between two parties, say, Alice and Bob. Its security relies on the basic property of quantum mechanics that information gain about a quantum state is only possible at the expense of changing the state, if the states to be distinguished are not orthogonal. The basic BB84 protocol goes as follows: (1) Alice randomly creates two strings of bitsB a andK a , each with size n.
(4) Bob randomly generates a string of bitsB b with size n.
(5) Bob measures each qubit received from Alice according to a basis determined by the bits he generated: if the ith bit ofB b is k then he measures with {|k 0 , |k 1 }, k = 0, 1. Let the measurement results bẽ K b , which is also a string of bits with size n.
(6) Bob sends his choice of measurement basesB b back to Alice, and upon receiving the information, Alice sends her basesB a to Bob.
(7) Alice and Bob determine at which positions the bit stringsB a andB b are equal. They discard the bits inK a andK b where the corresponding bits ofB a andB b do not match.
After the execution of the basic BB84 protocol above, the remaining bits ofK a andK b , denoted byK ′ a andK ′ b respectively, should be the same, provided that the channels used are perfect, and no eavesdropper exists.
To detect a potentially existing eavesdropper Eve, Alice and Bob proceed as follows: are the secure keys shared by Alice and Bob. Otherwise, an eavesdropper is detected, and the protocol halts without generating any secure keys.
For simplicity, we omit the processes of information reconciliation and privacy amplification. Now we describe the above protocol in our language of qCCS. To ease the notations, we assume a special measurement Ran[q;x] which can create a string of n random bits, independent of the initial states of theq system, and store it tox.
where Set n + is the super-operator which sets each of the n qubits it applies on to |+ , Mỹ[q;K b ] is the quantum measurement onq according to the basis determined byỹ, i.e., for each 1 ≤ k ≤ n, it measures q k with respect to the basis {|0 , |1 } (reps. {|+ , |− }) if y(k) = 0 (resp. 1), and stores the result intoK b (k). M n 0,1 is the same as M 0···0 , and Hỹ[q] has a similar meaning with Mỹ[q;K b ]. We also abuse the notion slightly by writing EB[q].P when we mean 1 ñ x=0 n (ifB =x then Ex[q].P ) where 0 n is the all zero string of size n. The function cmp takes a triple of stringsx,ỹ,z with the same size as inputs, and returns the substring ofx where the corresponding bits ofỹ andz match. Whenỹ andz match nowhere, we let cmp(x,ỹ,z) = ǫ, the empty string.  (key a !cmp The pLTSs of BB84 and BB84 spe for the special case of n = 2 can be depicted as in Figure 2, where for simplicity, we only specify the branch whereB a =K a = 00. Each arrow in the graph denotes a sequence of τ actions, and all probabilistic distributions are uniform. The strings at the bottom line are the outputs of the protocol. Then it can be easily checked from the pLTSs that BB84 ≈ o BB84 spe . The key is, for each extra branch in BB84 caused by the measurement of Bob (theK b line), the final states are bisimilar; they all output the same string.
The second choice is to use logic formulae. Let then suc!0.nil else f ail!0))\{key a , key b }, where true is the abbreviation of i∈∅ φ i . It is not difficult to show T estBB84 |= ψ p for any p > 0.
Now we proceed to describe the protocol where an eavesdropper can be detected. ,x).nil else alarm a !0.nil)))\{key a } where |x| is the size ofx, the function SubStr(K ′ a ,x) returns the substring ofK ′ a at the indexes specified byx, and RemStr(K ′ a ,x) returns the remaining substring ofK ′ a by deleting SubStr(K ′ a ,x). The special measurement P str m , which is similar to Ran, randomly generates a ⌈m/2⌉-sized string of indexes from 1, . . . , m.
For the capacity of a potential eavesdropper Eve, we assume that she has complete control of the quantum channel, but can only listen on the classical channels between Alice and Bob. That is, she can do any quantum operations on the communicated qubits from Alice and Bob, one of the extreme cases being keeping the qubits from Alice while creating and sending to Bob some fresh ones, with the same size, prepared by herself. But for classical communication, Eve can only copy and resend the bits without altering them, since Alice and Bob can choose to send them through a broadcasting channel. Note that perfect copying of the qubits transmitted through the quantum channel from Alice to Bob is prohibited by the basic laws of quantum mechanics, since the potential quantum states sent, |0 , |1 , |+ , and |− in this protocol, are nonorthogonal. With these natural assumptions, an eavesdropper Eve can be described as: where E is a super-operator, and gkey is the function Eve used to generate her guess of the key from the classical information transmitted between Alice and Bob. Then a practical running BB84 protocol, with the existence of an eavesdropper, goes as follows where f a and f b are relabelling functions such that f a (a2b) = a2e, f a (b2a) = e2a, f a (A2B) = A2E, and To get a taste of the security of BB84 ′ , we consider a special case where Eve's strategy is to simply measure the qubits sent by Alice, according to randomly guessed bases, to get the keys. She then prepares and sends to Bob a fresh sequence of qubits, employing the same method Alice used to encode keys, but using her own guess of bases and the keys she obtained. That is, we define It is generally very complicated to prove the security of the full BB84 protocol, even for the simplified Eve ′ presented above. Here we choose to reduce T estBB84 ′ to a simpler process which is easier for further verification. To be specific, we can show that T estBB84 ′ is bisimilar to the following process: where to ease the notations, we letK ab = cmp(K a ,B a ,B b ),K ba = cmp(K b ,B a ,B b ),Kx ab = SubStr(K ab ,x), andKx ba = SubStr(K ba ,x). Similar to Ran, the special measurement Ran ′ here, which takes three parameters, delivers a string of n bits. For example, RanB a,Be,Ka [q;K e ] will first generate a string of n − |K ae | random bitsx, replace withx the substring ofK a at the positions whereB a andB e do not match, and store the string after the replacement inK e .

Conclusion and related work
In our opinion, bisimulations should be considered as a proof methodology for demonstrating behavioural equivalence between systems, rather than providing the definition of the extensional behavioural equivalence itself. We have adapted the well-known reduction barbed congruence used for a variety of process calculi [20,32,11,5], to obtain a touchstone extensional behavioural equivalence for quantum processes considered in [10]. In the literature there are also minor variations on the formulation of reduction barbed congruence, often called contextual equivalence or barbed congruence. See [11,35] for a discussion of the differences.
We have defined a notion of open bisimulations, which provides both a sound and complete coinductive proof methodology for establishing the equivalence between qCCS processes. The operational semantics of this language is given in terms of probabilistic labelled transition systems. Moreover, we have generalised Hennessy-Milner logic to express the behaviour of quantum processes. In the resulting quantum logic, logical equivalence coincides with open bisimilarity.
To conclude this paper, we would like to compare the open bisimulation defined here with other bisimulations for quantum processes already proposed in the literature. Jorrand and Lalire [25,27] defined a branching bisimulation for their QPAlg, which identifies quantum processes whose associated graphs have the same branching structure. However, their bisimulation cannot always distinguish different quantum operations, as quantum states are only compared when they are input or output. More seriously, the derived bisimilarity is not a congruence; it is not preserved by restriction. Bisimulation defined in [9] indeed distinguishes different quantum operations but it works well only for finite processes, since quantum states are compared after all actions have been performed. Again, it is not preserved by restriction, and whether it is preserved by parallel composition still remains open, although the positive answer is affirmed in two special cases. In [41], a congruent (strong) bisimulation was proposed for a special model where no classical datum is involved. However, as many important quantum communication protocols such as superdense coding and teleportation cannot be described in that model, the scope of its application is very limited. Furthermore, as all quantum operations are regarded as visible in [41], the bisimulation is too strong; it distinguishes two different sequences of quantum operations even when they have the same effect as a whole.
The first general (works for general models where both classical and quantum data are involved, and recursive definition is allowed), weak (quantum operations are regarded as invisible, so that they can be combined arbitrarily), and congruent bisimulation for quantum processes was defined in [10]. It differentiates quantum input, to match which an arbitrarily chosen super-operator should be considered, from other actions. The open bisimulation in this paper makes a step further by treating the super-operator application in an 'open' style: applying super-operators before an action to be matched is selected. This makes it possible to separate ground bisimulation and the closedness under super-operator application, and by doing so, we are able to provide not only a neater and simpler definition, but also a powerful technique for proving bisimilarity.
It is easy to prove that the bisimulation in [10] is both a ground bisimulation and closed under superoperator application. Then by Proposition 5.5, it is also an open bisimulation; in other words, the bisimilarity presented in the current paper is coarser than that defined in [10]. Whether or not they are actually the same is an interesting question, and we leave it for further investigation.