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.