{'fraction_non_alphanumeric': 0.06203792992606879, 'fraction_numerical': 0.007221686488803171, 'mean_word_length': 3.749236718909017, 'pattern_counts': {'":': 0, '<': 1, '<?xml version=': 0, '>': 4, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 22, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Symbolic bisimulation for quantum processes

With the previous notions of bisimulation presented in literature, to check if two quantum processes are bisimilar, we have to instantiate the free quantum variables of them with arbitrary quantum states, and verify the bisimilarity of resultant configurations. This makes checking bisimilarity infeasible from an algorithmic point of view because quantum states constitute a continuum. In this paper, we introduce a symbolic operational semantics for quantum processes directly at the quantum operation level, which allows us to describe the bisimulation between quantum processes without resorting to quantum states. We show that the symbolic bisimulation defined here is equivalent to the open bisimulation for quantum processes in the previous work, when strong bisimulations are considered. An algorithm for checking symbolic ground bisimilarity is presented. We also give a modal logical characterisation for quantum bisimilarity based on an extension of Hennessy-Milner logic to quantum processes.


Introduction
An important issue in quantum process algebra is to discover a quantum generalisation of bisimulation preserved by various process constructs, in particular, parallel composition, where one of the major differences between classical and quantum systems, namely quantum entanglement, is present. Jorrand and Lalire [13,15] defined a branching bisimulation for their Quantum Process Algebra (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. Moreover, the derived bisimilarity is not a congruence; it is not preserved by restriction. Bisimulation defined in [7] indeed distinguishes different quantum operations but it works well only for finite processes. Again, it is not preserved by restriction. In [20], a congruent 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.
A general notion of bisimulation for the quantum process algebra qCCS developed by the authors was found in [8], which enjoys the following nice features: (1) it is applicable to general models where both classical and quantum data are involved, and recursion is allowed; (2) it is preserved by all the standard process constructs, including parallel composition; and (3) quantum operations are regarded as invisible, so that they can be combined arbitrarily. Independently, a bisimulation congruence in Communicating Quantum Processes (CQP), developed by Gay and Nagarajan [11], was established by Davidson [5]. Later on, motivated by [18], an open bisimulation for quantum processes was defined in [6] that makes it possible to separate ground bisimulation and the closedness under super-operator applications, thus providing not only a neater and simpler definition, but also a new technique for proving bisimilarity.
The various bisimulations defined in the literature, however, have a common shortcoming: they all resort to the instantiation of quantum variables by quantum states. As a result, to check whether or not two processes are bisimilar, we have to accompany them with an arbitrarily chosen quantum states, and check if the resultant configurations are bisimilar. Note that all quantum states constitute a continuum. The verification of bisimilarity is actually infeasible from an algorithmic point of view. The aim of the present paper is to tackle this problem by the powerful symbolic technique [12,4]. This paper only considers qCCS, but the ideas and techniques developed here apply to other quantum process algebras.
As a quantum extension of value-passing CCS, qCCS has both (possibly infinite) classical data domain and (doomed-to-be infinite) quantum data domain. The possibly infinite classical data set can be dealt with by symbolic bisimulation [12] for classical process algebras directly. However, in qCCS, we are also faced with the additional difficulty caused by the infinity of all quantum states. The current paper solves this problem by introducing super-operator valued distributions, which allows us to fold the operational semantics of qCCS into a symbolic version and provides us with a notion, also called symbolic bisimulation for simplicity, where to check the bisimilarity of two quantum processes, only a finite number of process-superoperator pairs need to be considered, without appealing to quantum states. To be specific, we propose • a symbolic operational semantics of qCCS in which quantum processes are described directly by the super-operators they can perform. It also incorporates a symbolic treatment for classical data.
• a notion of symbolic bisimulation, based on the symbolic operational semantics, as well as an efficient algorithm to check its ground version; • the coincidence of symbolic bisimulation with the open bisimulation defined in [6], when strong bisimulation is considered.
• a modal characterisation of symbolic bisimulation by a quantum logic as an extension of Hennessy-Milner logic.
The remainder of the paper is organised as follows. In Section 2, we review some basic notions from linear algebra and quantum mechanics. The syntax and (ordinary) operational semantics of qCCS are presented in Section 3. We also review the definition of open bisimulation presented in [6]. Section 4 collects some definitions and properties of the semiring of completely positive super-operators. The notion of super-operator valued distributions, which serves as an extension of probabilistic distributions, is also defined. Section 5 is the main part of this paper where we present a symbolic operational semantics of qCCS which describes the execution of quantum processes without resorting to concrete quantum states. Based on it, symbolic bisimulation between quantum processes, which also incorporates a symbolic treatment for classical data, motivated by symbolic bisimulation for classical processes, is presented and shown to be equivalent to the open bisimulation in Section 3. Section 6 is devoted to proposing an algorithm to check symbolic ground bisimulation, which is applicable to reasoning about the correctness of existing quantum communication protocols. In section 7 we propose a modal logic which turns out to be both sound and complete with respect to the symbolic bisimulation. We outline the main results in Section 8 and point out some directions for further study. In particular, we suggest the potential application of our results in model checking quantum communication protocols.

Preliminaries
For convenience of the reader, we briefly recall some basic notions from linear algebra and quantum theory which are needed in this paper. For more details, we refer to [16].

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; (2) φ|ψ = ψ|φ * ; 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 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 } constitute 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 λ i . A linear operator A ∈ L(H) is unitary if A † A = AA † = I H where I H is the identity operator on H. The trace of A 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 orthonormal basis selected. 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 , |φ 2 ∈ H 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.
Traditionally, a linear operator E on L(H) is called a super-operator on H. A super-operator is said to be 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 [14] of completely positive superoperators states that a super-operator E is completely positive if and only if there are some set of operators {E i : i ∈ I} with appropriate dimension such that The operators E i are called Kraus operators of E. We abuse the notation slightly by denoting E = {E i : i ∈ I}. A super-operator E is said to be trace-nonincreasing if tr(E(A)) ≤ tr(A) for any positive A ∈ L(H), and trace-preserving if the equality always holds. Equivalently, a super-operator is trace-nonincreasing completely positive (resp. trace-preserving completely positive) if and only if its Kraus operators In this paper, we will use some well-known (unitary) super-operators listed as follows: the quantum control-not super-operator CN = {C N } performed on two qubits where We also use the notations X , Z, and Y to denote σ 1 , σ 2 , and σ 3 , respectively.

Basic quantum mechanics
According to von Neumann's formalism of quantum mechanics [19], 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  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 which appears repeatedly in our examples of this paper. This kind of state is called entangled state.
To see the strangeness of entanglement, suppose a measurement M = λ 0 [|0 ] + λ 1 [|1 ] 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 [2] and super-dense coding [3]. 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.
its spectral decomposition. Obviously, the projectors {E m : m ∈ spec(M )} form a quantum measurement. If the state of a quantum system is ρ, then the probability that result m occurs when measuring M on the system is p(m) = tr(E m ρ), and the post-measurement state of the system is E m ρE m /p(m). Note that for each outcome m, the map is again a super-operator by Kraus Theorem; it is not trace-preserving in general. Let M be a projective measurement with Eq.(1) its spectral decomposition. We call M nondegenerate if for any m ∈ spec(M ), the corresponding projector E m is 1-dimensional; that is, all eigenvalues of M are non-degenerate. 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.

qCCS: Syntax and Semantics
In this section, we review the syntax and semantics of a quantum extension of value-passing CCS, called qCCS, introduced in [7,20,8], and the definition of open bisimulation between qCCS processes presented in [6].

Syntax
We assume three types of data in qCCS: Bool for booleans, real numbers Real for classical data, and qubits Qbt for quantum data. Let cV ar, ranged over by x, y, . . . , be the set of classical variables, and qV ar, ranged over by q, r, . . . , the set of quantum variables. It is assumed that cV ar and qV ar are both countably infinite. We assume a set Exp of classical data expressions over Real, which includes cV ar as a subset and is ranged over by e, e ′ , . . . , and a set of boolean-valued expressions BExp, ranged over by b, b ′ , . . . , with the usual set of boolean operators tt, ff, ¬, ∧, ∨, 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. Let cChan be the set of classical channel names, ranged over by c, d, . . . , and qChan the set of quantum channel names, ranged over by c, d, . . . . Let Chan = cChan ∪ qChan. A relabeling function f is a one to one function from Chan to Chan such that f (cChan) ⊆ cChan and f (qChan) ⊆ qChan.
We often abbreviate the indexed set {q 1 , . . . , q n } to q when q 1 , . . . , q n are distinct quantum variables and the dimension n is understood. Sometimes we also use q to denote the string q 1 . . . q n . We assume a set of process constant schemes, ranged over by A, B, . . . . Assigned to each process constant scheme A there are two non-negative integers ar c (A) and ar q (A). If x is a tuple of classical variables with | x| = ar c (A), and q a tuple of distinct quantum variables with | q| = ar q (A), then A( x, q) is called a process constant. When ar c (A) = ar q (A) = 0, we also denote by A the (unique) process constant produced by A.
Based on these notations, the syntax of qCCS terms can be given by the Backus-Naur form as where c ∈ cChan, x ∈ cV ar, c ∈ qChan, q ∈ qV ar, q ⊆ qV ar, e ∈ Exp, e ⊆ Exp, τ is the silent action, A( x, q) is a process constant, f is a relabeling function, L ⊆ Chan, b ∈ BExp, and E and M are respectively a trace-preserving super-operator and a non-degenerate projective measurement applying on the Hilbert space associated with the systems q. In this paper, we assume all superoperators are completely positive. To exclude quantum processes which are not physically implementable, we also require q ∈ qv(t) in c!q.t and qv(t) ∩ qv(u) = ∅ in t u, where for a process term t, qv(t) is the set of its free quantum variables inductively defined as follows: qv(A( e, q)) = q.
The notion of free classical variables in quantum processes, denoted by f v(·), can be defined in the usual way with the only modification that the quantum measurement prefix M [ q; x] has binding power on x. A quantum process term t is closed if it contains no free classical variables, i.e., f v(t) = ∅. We let T , ranged over by t, u, · · · , be the set of all qCCS terms, and P, ranged over by P, Q, · · · , the set of closed terms. To complete the definition of qCCS syntax, we assume that for each process constant A( x, q), there is a defining equation such that f v(t) ⊆ x and qv(P ) ⊆ q. Throughout the paper we implicitly assume the convention that process terms are identified up to α-conversion.
The process constructs we give here are quite similar to those in classical CCS, and they also have similar intuitive meanings: nil stands for a process which does not perform any action; c?x and c!e are respectively classical input and classical output, while c?q and c!q are their quantum counterparts. E[ q] denotes the action of performing the super-operator E on the qubits q while M [ q; x] measures the qubits q according to M and stores the measurement outcome into the classical variable x. + models nondeterministic choice: t + u behaves like either t or u depending on the choice of the environment. denotes the usual parallel composition. The operators \L and [f ] model restriction and relabeling, respectively: t\L behaves like t as long as any action through the channels in L is forbidden, and t[f ] behaves like t where each channel name is replaced by its image under the relabeling function f . Finally, if b then t is the standard conditional choice where t can be executed only if b is tt.
An evaluation ψ is a function from cV ar to Real; it can be extended in an obvious way to functions from Exp to Real and from BExp to {tt, ff}, and finally, from T to P. For simplicity, we still use ψ to denote these extensions. Let ψ{v/x} be the evaluation which differs from ψ only in that it maps x to v.

Transitional semantics
For each quantum variable q ∈ qV ar, we assume a 2-dimensional Hilbert space H q to be the state space of the q-system. For any S ⊆ qV ar, we denote In particular, H = H qV ar is the state space of the whole environment consisting of all the quantum variables. Note that H is a countably-infinite dimensional Hilbert space.
Suppose P is a closed quantum process. A pair of the form P, ρ is called a configuration, where ρ ∈ D(H) is a density operator on H. The set of configurations is denoted by Con, and ranged over by C, D, · · · . Let For each α ∈ Act c , we define the bound quantum variables qbv(α) of α as qbv(c?r) = {r} and qbv(α) = ∅ if α is not a quantum input. The channel names used in action α is denoted by cn(α); that is, cn(c?v) = cn(c!v) = {c}, cn(c?r) = cn(c!r) = {c}, and cn(τ ) = ∅. We also extend the relabelling function to Act c in an obvious way.
Let Dist(Con), ranged over by µ, ν, · · · , be the set of all finite-supported probabilistic distributions over Con. Then the operational semantics of qCCS can be given by the probabilistic labelled transition system (pLTS) Con, Act c , −→ , where −→ ⊆ Con × Act c × Dist(Con) is the smallest relation satisfying the inference rules depicted in Fig. 1. The symmetric forms for rules P ar c , C-Com c , Q-Com c , and Sum c are omitted.
In these rules, we abuse the notation slightly by writing where µ is the simple distribution such that µ(D) = 1. We also use the obvious extension of the function Figure 1: Operational semantics of qCCS on configurations to distributions. To be precise, if µ = i∈I p i P i , ρ i then µ Q denotes the distribution i∈I p i P i Q, ρ i . Similar extension applies to µ[f ] and µ\L.

Open bisimulation
In this subsection, we recall the basic definitions and properties of open bisimulation introduced in [6]. Let R ⊆ Con × Con be a relation on configurations. We can lift R to a relation on Dist(Con) by writing µRν if Note that here the set of C i , i ∈ I, are not necessarily distinct.
To illustrate the operational semantics and open bisimulation presented in this section, we give a simple example.
where Set 0 = {|0 0|, |0 1|}, M 0,1 is the 1-qubit measurement according to the computational basis {|0 , |1 }, I is the identity super-operator, and X is the Pauli-X super-operator. For any ρ ∈ D(H), the pLTSs rooted by P, ρ and Q, ρ respectively are depicted in Fig. 2 where .nil, and p i = tr(|i q i|ρ). We can show P∼ Q by verifying that the relation R ∪ R −1 , where  We alway omit the symbol • and write AB directly for A•B. Furthermore, the operation • is (both left and right) distributive with respect to +: Thus (CP (H), +, •) forms a semiring.
For any A, B ∈ CP (H) and V ⊆ qV ar, we write A V B if for any ρ ∈ D(H), tr V (A(ρ)) ⊑ tr V (B(ρ)), where V is the complement set of V in qV ar, and ⊑ is the Löwner preorder defined on operators such as The following proposition is direct from definitions: , tr(A(ρ)) = tr(ρ) for any ρ ∈ D(H).
The next lemma, which is easy from definition, shows that the equivalence relation V is preserved by right application of composition.
However, is not preserved by composition from the left-hand side. A counter-example is when A is the X-pauli super-operator, and C has one single Kraus operator |0 0|. Then A I H , but CA CI H since tr(CA(|0 0|)) = 0 while tr(CI H (|0 0|)) = 1. Nevertheless, we have the following property which is useful for latter discussion.
It is easy to check that for any E, F ∈ CP t (H) and V ⊆ qV ar, E V F if and only if E V F . So for trace-preserving super-operators, we usually use the more symmetric form V instead of V .

Super-operator valued distributions
Let S be a countable set. A super-operator valued distribution, or simply distribution for short, ∆ over S is a function from S to CP (H) such that s∈S ∆(s) I H . We denote by ⌈∆⌉ the support set of ∆, i.e., the set of s such that ∆(s) = 0 H . Let Dist H (S) be the set of finite-support super-operator valued distributions over S; that is, Let ∆, Ξ, etc range over Dist H (S). When ∆ is a simple distribution such that ⌈∆⌉ = {s} for some s and ∆(s) = E, we abuse the notation slightly to denote ∆ by E • s. We further abbreviate I H • s to s. Note that there are infinitely many different simple distributions having the same support {s}. Here and in the following of this paper, the index sets I, J, K, etc are all assumed to be finite. By Lemma 4.2, it is easy to check that the above definition is well-defined. Furthermore, since is not preserved by left applications of composition, we cannot require ∆(s) = i∈I A i ∆ i (s) in the second clause, although it seems more natural. As a result, say, Probability distributions can be regarded as special super-operator valued distributions by requiring that all super-operators appeared in the definitions above have the form pI H where 0 ≤ p ≤ 1. Since in this case all super-operators commute, we always omit the bullet • in the expressions.

Super-operator weighted transition systems
We now extend the ordinary probabilistic labelled transition systems to super-operator weighted ones.
Definition 5.1. A super-operator weighted labelled transition system, or quantum labelled transition system (qLTS), is a triple (S, Act, −→), where (1) S is a countable set of states, (2) Act is a countable set of transition actions, For simplicity, we write s α −→ ∆ instead of (s, α, ∆) ∈−→. A pLTS may be viewed as a degenerate qLTS in which all super-operator valued distributions are probabilistic ones.

Symbolic transitional semantics of qCCS
To present the symbolic operational semantics of quantum processes, we need some more notations. Let Act s = {τ } ∪ {c?x, c!e | c ∈ cChan, x ∈ cV ar, e ∈ Exp} ∪ {c?r, c!r | c ∈ qChan, r ∈ qV ar} and BAct s = BExp × Act s . For each γ ∈ Act s , the notion qbv(γ) for bound quantum variables, cn(γ) for channel names, and f v(γ) for free classical variables are similarly defined as for Act c . We also define bv(γ), the set of bound classical variables in γ in an obvious way.
A pair of the form t, E , where t ∈ T and E ∈ CP t (H), is called a snapshot, and the set of snapshots is denoted by SN . Then the symbolic semantics of qCCS is given by the qLTS (SN, BAct s , −→) on snapshots, where −→ ⊆ SN × BAct s × Dist H (SN ) is the smallest relation satisfying the rules defined in Fig. 3. In Rule M eas s , for each i ∈ I, A φi r ∈ CP (H) and Set φi r ∈ CP t (H) are defined respectively as The symmetric forms for rules P ar s , C-Com s , Q-Com s , and Sum s are omitted. Here again, the functions , [f ], and \L have been extended to super-operator valued distributions by denoting, say, The transition graph of a snapshot is depicted as usual where each transition t, We sometimes omit the line marked with I H for simplicity.
Example 5.2. (Example 3.3 revisited) For the first example, we revisit the two ways of setting a quantum system to pure state |0 , presented in Example 3.3. According to the symbolic operational semantics presented in Fig. 3, the qLTSs rooted by P, I H and Q, I H respectively can be depicted as in Fig. 4, where A i has the single Kraus operator |i q i| for i = 0, 1.
At the first glance, it is tempting to think that symbolic semantics provides no advantage in describing quantum processes, as the qLTSs in Fig. 4 are almost the same as the pLTSs in Fig. 2 (Indeed, the right-hand side qLTS in the former is even more complicated than the corresponding pLTS in the latter). However, pLTSs in Fig. 2 are depicted for a fixed quantum state ρ; to characterise the behaviours of a quantum process, infinitely many such pLTSs must be given, although typically they share the same structure. On the other hand, the qLTSs in Fig. 4 specify all possible behaviours of the processes, by means of the super-operators they can perform.  coding protocol can be defined as follows: The specification of super-dense coding protocol can be defined as: Here Set i and Set Ψ are the 2-qubit super-operators which set the target qubits to | i and |Ψ = (|00 + |11 )/ √ 2, respectively. We insert seven τ 's in the specification to match the internal actions of Sdc. The qLTSs rooted from Sdc spec , I H and Sdc, I H respectively are depicted in Fig. 5 where q = {q 1 , q 2 }, A i is the super-operator with the single Kraus operator | i i|, L = {c A , c B , e}, ].e!q 1 .nil) Bob \{e}, and for simplicity, we only draw the transitions along the x = 0 branch.
To conclude this subsection, we prove some useful properties of symbolic transitions.
tt, τ 3 ❄ Figure 5: qLTSs for Sdc spec , I H and Sdc, I H Especially, if |I| > 1 then B i and F i take the forms as A φi r and Set φi r in Eqs. (2) and (3), respectively.
Proof. Easy from the definition of inference rules. ✷ The following lemmas show the relationship between transitions in ordinary semantics and in symbolic semantics. Let ψ be an evaluation, α ∈ Act c , and γ ∈ Act s . We write α = ψ γ if either α = c!v, γ = c!e, and ψ(e) = v, or γ = α if neither of them is a classical output.
Proof. We prove by induction on the depth of the inference by which the action tψ, ρ α −→ µ is inferred. We argue by cases on the form of t.
(1) t = c?x.t ′ . Then tψ = c?x.u where u is the process term obtained from t ′ by instantiating all the free variables in f v(t ′ ) − {x} according to ψ. By Rule C-Inp c we deduce that α = c?v for some v ∈ Real and µ = P, ρ where P = u{v/x} = t ′ ψ{v/x}. By Rule Act s , for any (2) t = c!e.t ′ . Then tψ = c!ψ(e).(t ′ ψ), and by Rule C-Out c we deduce that α = c!ψ(e) and µ = t ′ ψ, ρ . By Rule Act s , for any E ∈ CP t (H), we have t, E tt,c!e −→ t ′ , E . So we need only to take b = tt, |I| = 1, t i = t ′ , A i = E i = I H as well.

Symbolic bisimulation
Let S ⊆ SN × SN be an equivalence relation. We lift S to Dist H (SN ) × Dist H (SN ) by defining ∆SΞ if for any equivalence class T ∈ SN/S, ∆(T ) Ξ(T ); that is, t,E ∈T ∆( t, E ) t,E ∈T Ξ( t, E ). We write γ = b γ ′ if either γ = c!e, γ ′ = c!e ′ , and b → e = e ′ , or γ = γ ′ if neither of them is a classical output.  (2) for any G ∈ CP t (H qv(t) ), whenever t, GE Two configurations t, E and u, F are symbolically b-bisimilar, denoted by t, E ∼ b u, F , if there exists a symbolic bisimulation S = {S b : b ∈ BExp} such that t, E S b u, F . Two quantum process terms t and u are symbolically b-bisimilar, denoted by t ∼ b u, if t, I H ∼ b u, I H . When b = tt, we simply write t ∼ u.
To show the usage of symbolic bisimulation, we revisit the examples presented in Section 5.2 to show that the proposed protocols indeed achieve the desired goals. Let A = {A i : i ∈ I} be a set of disjoint subsets of snapshots. An equivalence relation S is said to be generated by A if its equivalence classes on the set of snapshots ∪ i∈I A i are given by the partition A, and it is the identity relation on SN − ∪ i∈I A i . In the following, we denote by S * the equivalence closure of a relation S.
Lemma 5.11. Let S = {S b : b ∈ BExp} be a symbolic bisimulation. Then there exists a decreasing symbolic bisimulation U Obviously, U = {U b : b ∈ BExp} is decreasing. We have to show that U is a symbolic bisimulation. Let b ∈ BExp and t, E U b u, F . Note that U b 1 is both reflexive and symmetric. So U b is actually the transitive closure of U b 1 , and there exist n ≥ 1 and a sequence of snapshots t i , E i , 0 ≤ i ≤ n, such that t, E = t 0 , E 0 , u, F = t n , E n , and for each 0 For the sake of simplicity, we assume n = 2. That is, there exists s, G such that t, E S b1 s, The general case is more tedious but similar.
First we check that if b is satisfiable, then qv(t) = qv(s) = qv(u) and E qv(t) G qv(t) F . Now we may assume further that bv(γ) ∩ f v(s) = ∅. From t, E S b1 s, G , there exists a collection of booleans . By α-conversion, we can again assume that for each i, bv(γ i ) ∩ f v(b 2 , s, u) = ∅. Now by the assumption that s, G S b2 u, F , there exists a collection of booleans Proof. Let b ∈ BExp and t, E (S b 1 S b 2 ) * u, F . Suppose there exist n ≥ 1 and a sequence of snapshots t i , E i , 0 ≤ i ≤ n, such that t, E = t 0 , E 0 , u, F = t n , E n , and for each 0 ≤ i ≤ n − 1, Again, for the sake of simplicity, we assume n = 1. That is, there exists s, G such that t, E S b 1 s, G S b 2 u, F . The rest of the poof follows almost the same lines of those in Lemma 5.11, by employing the assumption that S 1 and S 2 are both decreasing. Proof. Easy from definition. ✷ Corollary 5.14.
With the lemmas above, we can show that the family {∼ b : b ∈ BExp} is actually the largest symbolic bisimulation. (2) The family {∼ b : b ∈ BExp} is a symbolic bisimulation.
Proof. (2) is direct from (1). To prove (1), let b ∈ BExp. Obviously, ∼ b is reflexive and symmetric. To show the transitivity of ∼ b , let t, E ∼ b u, F and u, F ∼ b s, G . Then by definition, there exist symbolic bisimulations S i = {S b i : b ∈ BExp}, i = 1, 2, such that t, E S b 1 u, F and u, F S b 2 s, G . By Lemma 5.11, we can assume without loss of generality that both S 1 and S 2 are decreasing, thus S = {(S b 1 S b 2 ) * : b ∈ BExp} is also a symbolic bisimulation, by Lemma 5.12. So t, E ∼ b s, G .
✷ To conclude this subsection, we present a property of symbolic bisimilarity which is useful for the next section.  (2) for any G ∈ CP t (H qv(t) ), whenever t, GE (3) Symmetric condition of (2).

Connection of symbolic and open bisimulations
To ease notation, in the rest of the paper we use t, u to range over SN , and sometimes equate t with t, E , u with u, F , ∆ with i∈I A i • t i , E i , and Ξ with j∈J B j • u j , F j without stating them explicitly. We also write (∆ψ)(ρ) = i∈I tr(A i (ρ)) t i ψ, E i (ρ) and (Ξψ)(ρ) = j∈J tr(B j (ρ)) u j ψ, F j (ρ) .
Let S = {S b : b ∈ BExp} be a symbolic bisimulation. Define We prove that R S is an open bisimulation. To achieve this, the following lemma is needed.
We decompose the set ⌈∆⌉ ∪ ⌈Ξ⌉ into disjoint subsets S 1 , · · · , S n such that any two snapshots are in the same S k if and only if they are related by S b . For each 1 ≤ k ≤ n, let For any ρ ∈ D(H) and ψ such that ψ(b) = tt, Similarly, we have Note that by definition, if tS b u then (tψ)(ρ)R S (uψ)(ρ). It follows that for any 1 ≤ k ≤ n, i ∈ K k ∩ I, and j ∈ K k ∩ J, we have t i ψ, E i (ρ) R S u j ψ, F j (ρ) . Furthermore, by Eq.(4), we know i∈K k ∩I tr(A i (ρ)) = j∈K k ∩J tr(B j (ρ)). Thus (∆ψ)(ρ) R S (Ξψ)(ρ) by definition. (2) For any G ∈ CP t (H qv(tψ) ), let Then by Lemma 5.5, we have Furthermore, we have γ = c?x for some x ∈ f v(t) and ψ ′ = ψ{v/x} if α = c?v, or γ = ψ α and ψ ′ = ψ otherwise. Note that if γ = c?x, we can always take x such that x ∈ f v(t, u, b) by α-conversion. Now by the assumption that tS b u, there exists a collection of booleans B such We can always find a b ′ ∈ B such that ψ(b ′ ) = tt, and so ψ(b 2 ) = tt as well. Then by Lemma 5.6, we have where β = c?v and ψ ′′ = ψ{v/x} if γ ′ = c?x, or γ ′ = ψ β and ψ ′′ = ψ otherwise.
Proof. (2) and (3)   We prove that S∼ = {S b∼ : b ∈ BExp} is a symbolic bisimulation. Firstly, it is easy to check that for each b, S b∼ is an equivalence relation. Two quantum states ρ, σ ∈ D(H) are said to be equal except at q if tr q ρ = tr q σ. Then we can show the following lemma, which is parallel to Lemma 5.17. Proof. Let ∆ = i∈I A i • t i , E i and Ξ = j∈J B j • u j , F j . We prove this lemma by distinguishing two cases: (1) Both |I| > 1 and |J| > 1. Similar to Lemma 5.17, we first decompose the set ⌈∆⌉ ∪ ⌈Ξ⌉ into disjoint subsets S 1 , · · · , S n such that any two snapshots are in the same S k if and only if they are related by S b∼ . For each 1 ≤ k ≤ n, let and K = {K k : 1 ≤ k ≤ n}. Note that by Lemma 5.4, there are two sets of pairwise orthogonal pure states {|φ i : i ∈ I} and {|φ ′ j : j ∈ J} in some H q such that the Kraus operators of Then it suffices to show E k = F k , 1 ≤ k ≤ n. In the following, we prove E 1 = F 1 ; other cases are similar.
As the effects of the super-operators A i and B j are simply erasing the original information at q and setting the partial states of q to be |φ i and |φ ′ j , respectively, we have L ψ,ρ = L ψ,σ (which means m ψ ρ = m ψ σ , and L ψ,ρ l = L ψ,σ l for each l) for all σ which is equal to ρ except at q. Note that tr(A i (ρ)) = tr(|φ i q φ i |ρ) = tr(|φ i q φ i |ρ q ) where ρ q = tr q ρ is the reduced state of ρ at the systems q. Let E ψ,ρ 1 = k∈I ψ,ρ E k and F ψ,ρ 1 = k∈I ψ,ρ F k . Then for any ρ ′ ∈ D(H q ), where σ = ρ ′ ⊗ tr q (ρ) is equal to ρ except at q, and the second equality is from the assumption that (∆ψ)(σ)∼ (Ξψ)(σ). This implies E 1 + E ψ,ρ We claim that K = ∅. Otherwise, there exists k such that k ∈ I ψ,ρ for any ψ(b) = tt and ρ. Then by the definition of L ψ,ρ contradicting the fact that they belong to different equivalence classes of S b∼ . Now for any pure state |φ such that E 1 |φ = |φ , we have E ψ,ρ 1 |φ = 0 for any ρ and ψ(b) = tt, by the orthogonality of E i 's. Thus F ψ,ρ and finally, k∈K F k |φ = |φ − F 1 |φ . Then F 1 |φ = |φ from the fact that K = ∅. Similarly, we can prove that for any |φ , F 1 |φ = |φ implies E 1 |φ = |φ . Thus E 1 = F 1 .
(2) For any G ∈ CP t (H qv(t) ), let with bv(γ) ∩ f v(b, t, u) = ∅. We need to construct a set of booleans B such that b ∧ b 1 → B, Here similar to [12], to ease the notations we only consider the case where for each Θ, there is at most one symbolic action, denoted by (b(Θ), γ(Θ)), such that u, GF b(Θ),γ(Θ) −→ Θ. For each Θ ∈ U , let b ′ Θ be a boolean expression such that for any ψ, whereψ = ψ{v/x} for some v if γ = c?x, andψ = ψ otherwise.
(2) t ∼ u if and only if t∼ u.
(3) P ∼ b Q if and only if P∼ Q, provided that b is satisfiable.

An algorithm for symbolic ground bisimulation
From Clause (2) of Definition 5.7, to check whether two snapshots are symbolically bisimilar, we are forced to compare their behaviours under any super-operators. This is generally infeasible since all super-operators constitute a continuum, and it seems hopeless to design an algorithm which works for the most general case. In this section, we develop an efficient algorithm for a class of quantum process terms which covers all existing practical quantum communication protocols. To this end, we first define the notion of symbolic ground bisimulation which stems from [18].
Given two configurations t, E and u, F , we write t, E ∼ b g u, F if there exists a symbolic ground bisimulation {S b : b ∈ BExp} such that t, E S b u, F . Definition 6.2. A relation S on SN is said to be closed under super-operator application if t, E S u, F implies t, GE S u, GF for any G ∈ CP t (H qv(t) ). A family of relations are closed under superoperator application if each individual relation is.
The following proposition, showing the difference of symbolic bisimulation and symbolic ground bisimulation, is easy from definition. Proposition 6.3. ∼ is the largest symbolic ground bisimulation that is closed under super-operator application.
A process term is said to be free of quantum input if all of its descendants, including itself, can not perform quantum input actions. Note that all existing quantum communication protocols such as super-dense coding [3], teleportation [2], quantum key-distribution protocols [1], etc, are, or can easily modified to be, free of quantum input. Putting this constraint will not bring too much restriction on the application range of our algorithm. Lemma 6.4. Let t, E ∼ b g u, F , and t and u both free of quantum input. Then for any G ∈ CP t (H qv(t) ), t, GE ∼ b g u, GF .
Proof. We need to show GE , u, GF ) : t and u free of quantum input, G ∈ CP t (H qv(t) ), and t, E ∼ b g u, F }, is a symbolic ground bisimulation. This is easy by noting that for any descendant t ′ of t, qv(t ′ ) ⊆ qv(t), and then G ∈ CP t (H qv(t ′ ) ) as well. Consequently, G commutes with all the super-operators performed by t and its descendants. ✷ Theorem 6.5. If t and u are both free of quantum input, then t, Proof. Easy from Lemma 6.4. ✷ Algorithm 1 computes the most general boolean b such that t ∼ b g u, for two given snapshots t and u. By the most general boolean mgb(t, u) we mean that t ∼ mgb(t,u) g u and whenever t ∼ b g u then b → mgb(t, u). From Theorem 6.5, this algorithm is applicable to verify the correctness of all existing quantum communication protocols.
The algorithm closely follows that introduced in [12]. The main procedure is Bisim(t, u). It starts with the initial snapshot pairs (t, u), trying to find the smallest symbolic bisimulation relation containing the pair by comparing transitions from each pair of snapshots it reaches. The core procedure Match has four parameters: t and u are the current terms under examination; b is a boolean expression representing the constraints accumulated by previous calls; W is a set of snapshot pairs which have been visited. For each possible action enabled by t and u, the procedure MatchAction is used to compare possible moves from t and u. Each comparison returns a boolean and a table; the boolean turns out to be mgb(t, u) and the table is used to represent the witnessing bisimulation. We consider a table as a function that maps a pair of snapshots to a boolean. The disjoint union of tables, viewed as sets, is denoted by ⊔.
The main difference from the algorithm of [12] lies in the comparison of τ transitions. We introduce the procedure MatchDistribution to approximate ∼ b g by a relation R. For any two snapshots t i ∈ ⌈∆⌉ and u j ∈ ⌈Θ⌉, they are related by R if b → T (t i , u j ). More precisely, we use the equivalence closure of R instead in order for it to be used in the procedure Check. Moreover, if a snapshot pair (t, u) has been visited before, i.e. (t, u) ∈ W , then T (t, u) is assumed to be tt in all future visits. Hence, R is coarser than ∼ b g in general. We use Check(∆, Θ, R) to computate the constraint so that the super-operator valued distribution ∆ is related to Θ by a relation lifted from R. The correctness of the algorithm is stated in the following theorem. Theorem 6.6. For two snapshots t and u, the function Bisim(t, u) terminates. Moreover, if Bisim(t, u) = (θ, T ) then T (t, u) = θ = mgb(t, u).
Proof. Termination is easy to show. Each time a new snapshot pair is encountered, the procedure Match is called and the pair is added to the set W . Since we are considering a finitary transition graph, the number of different pairs is finite. Eventually every possible pair is in W and each call to Match immediately terminates.
Correctness of the algorithm is largely similar to that in [12], though we use the additional procedure MatchDistribution to compute the constraint that relates two super-operator valued distributions. ✷

Modal characterisation
We now present a modal logic to characterise the behaviour of quantum snapshots and their distributions.
With this lemma, we can show that the logic L exactly characterises the behaviours of quantum snapshots up to symbolic bisimilarity. Proof. We first prove the necessity part. For any φ, Φ ∈ L, it suffices to prove the following two properties: We proceed by mutual induction on the structures of φ and Φ. Take arbitrarily t ∼ b u, ∆ ∼ b Ξ, and ψ(b) = tt. Let t = t, E , u = u, F , ψ, t |= φ, and ψ, ∆ |= Φ. There are seven cases to consider: • φ = G q . Then qv(t) ∩ q = ∅ and E q G. Since t ∼ b u and b is satisfiable, we have qv(t) = qv (u) and E qv(t) F . Thus qv(u) ∩ q = ∅, and F q G from the fact that q ⊆ qv(t). Then ψ, u |= G q follows.
Finally, we prove that R is closed under super-operator application. To this end, we only need to show that = ψ L is ; that is, for any G ∈ CP t (H qv(t) ), t = ψ L u implies G(t) = ψ L G(u). Suppose t = ψ L u and let φ be a formula such that ψ, G(t) |= φ. Then ψ, t |= G.φ. It follows from t = ψ L u that qv(t) = qv(u) and ψ, u |= G.φ. Therefore, ψ, G(u) |= φ. By symmetry if φ is satisfied by ψ, G(u) then it is also satisfied by ψ, G(t). In other words, we have G(t) = ψ L G(u). Then R is an open bisimulation by Proposition 5 of [6]. ✷ For any t, u ∈ T and b ∈ BExp, we write t = b L u if for any evaluation ψ, ψ(b) = tt implies t, I H = ψ L u, I H . Then we have the following theorem: Theorem 7.5. For any t, u ∈ T , t ∼ b u if and only if t = b L u.

Conclusion and further work
The main contribution of this paper is a notion of symbolic bisimulation for qCCS, a quantum extension of classical value-passing CCS. By giving the operational semantics of qCCS directly by means of the super-operators a process can perform, we are able to assign to each (non-recursively defined) quantum process a f inite super-operator weighted labelled transition system, comparing to the inf inite probabilistic labelled transition system in previous literature. We prove that the symbolic bisimulation in this paper coincides with the open bisimulation in [6], thus providing a practical way to decide the latter. We also design an algorithm to check symbolic ground bisimulation, which is applicable to reasoning about the correctness of existing quantum communication protocols. A modal logic characterisation for the symbolic bisimulation is also developed.
A natural extension of the current paper is to study symbolic weak bisimulation where the invisible actions, caused by internal (classical and quantum) communication as well as quantum operations, are abstracted away. To achieve this, we may need to define symbolic weak transitions similar to those proposed in [8] and [6]. Note that one of the distinct features of weak transitions for probabilistic processes is the so-called left decomposibility; that is, if µ =⇒ ν and µ = i∈I p i µ i is a probabilistic decomposition of µ, then ν can be decomposed into i∈I p i ν i accordingly such that µ i =⇒ ν i for each i ∈ I. This property is useful in proving the transitivity of bisimilarity. However, it is not satisfied by symbolic transitions defined in this paper, since, in general, a super-operator does not have an inverse. Therefore, we will have to explore other ways of defining weak symbolic transitions, which is one of the research directions we are now pursing.
We have presented in this paper, for the first time in literature to the best of our knowledge, the notion of super-operator weighted labelled transition systems, which serves the semantic model for qCCS and plays an important role in describing and reasoning about quantum processes. For the next step, we are going to explore the possibility of model checking quantum communication protocols based on this model. As is well known, one of the main challenges for quantum model checking is that the set of all quantum states, traditionally regarded as the underlying state space of the models to be checked, is a continuum, so that the techniques of classical model checking, which normally works only for finite state space, cannot be applied directly. Gay et al. [9,10,17] provided a solution for this problem by restricting the state space to a set of finitely describable states called stabiliser states, and restricting the quantum operations applied on them to the class of Clifford group. By doing this, they were able to obtain an efficient model checker for quantum protocols, employing purely classical algorithms. The limit of their approach is obvious: it can only check the (partial) behaviours of a protocol on stabiliser states, and does not work for general protocols.
Our approach of treating both classical data and quantum operations in a symbolic way provides an efficient and compact way to describe behaviours of a quantum protocol without resorting to the underlying quantum states. In this model, all existing quantum protocols have finite state spaces, and consequently, classical model checking techniques will be easily adapted to verifying quantum protocols.