An Axiomatization for Quantum Processes to Unifying Quantum and Classical Computing

Abstract

We establish an axiomatization for quantum processes, which is a quantum generalization of process algebra ACP (Algebra of Communicating Processes). We use the framework of a quantum process configuration 〈p, ϱ〉, but we treat it as two relative independent part: the structural part p and the quantum part ϱ, because the establishment of a sound and complete theory is dependent on the structural properties of the structural part p. We let the quantum part ϱ be the outcomes of execution of p to examine and observe the function of the basic theory of quantum mechanics. We establish not only a strong bisimilarity for quantum processes, but also a weak bisimilarity to model the silent step and abstract internal computations in quantum processes. The relationship between quantum bisimilarity and classical bisimilarity is established, which makes an axiomatization of quantum processes possible. An axiomatization for quantum processes called qACP is designed, which involves not only quantum information, but also classical information and unifies quantum computing and classical computing. qACP can be used easily and widely for verification of most quantum communication protocols.

1 Introduction

The basic principles of quantum mechanics are widely adopted in computation and communication. As a relative novel computation pattern, quantum computing [21] brings the dawn of solving the so-called NP problem because of the strong parallel computation power of quantum computing. And also, many basic principles of quantum mechanics, such as Heisenberg uncertainty principle and quantum no-cloning theorem, provide quantum communication protocols the so-called provable security. Now, some quantum communication protocols, especially quantum key distribution protocols, have already been commercially available.

Process algebra [1] is well known in capturing traditional computation, especially parallelism and concurrence, in an interleaving pattern, such as CCS (Calculus of Concurrent Process) [2, 3], CSP (Communicating Sequential Processes) [4] and ACP (Algebra of Communicating Processes) [5]. To unify quantum computing and classical computing under the same process algebra framework, is attractive and has an important significance, because most quantum communication protocols involve quantum information and classical information, quantum computing and classical computing.

In this paper, we design an axiomatization called qACP for quantum processes with a quantum generalization of process algebra ACP, which unifies quantum computing and classical computing. qACP consists of not only an operational semantics based on classical structural operational semantics, but also an equational logic, by use of which, most quantum communication protocols can be verified easily.

This paper is organized as follows. In Section 2, we introduce the related works. We do not repeat some preliminaries, including basic concepts and conclusions about basic linear algebra, basic quantum mechanics, equational logic, structural operational semantics and process algebra ACP, please refer to [5, 6] for details. In Section 3, we extend classical structural operational semantics to support quantum processes. The basic quantum process algebra (BQPA) is introduced in Section 4, Quantum Process Algebra with Parallelism (QPAP) and Algebra of Quantum Communicating Processes (AQCP) are designed in Section 5. To capture infinite computing in quantum processes, we discuss recursion in Section 6. To model silent step and abstract internal computation, silent step and abstraction operator are introduced in Section 7. We unify qACP and classical ACP in Section 8. An example of the famous BB84 protocol [18] is verified by use of qACP in Section 9. qACP can be extended easily in an elegant way, which is shown in Section 10. Finally, we conclude this paper in Section 11.

2 Related Works

Quantum process algebra provides formal tools for modeling, analysis and verification of quantum communication protocols, which combines quantum communications and quantum computing together. Gay and Nagarajan [9, 10] defined a language called CQP (Communicating Quantum Processes) by adding primitives for quantum measurements and transformation of quantum states to π-calculus. An operational semantics and a type system for CQP were also presented to prove that the semantics preserves typing and typing guarantees that each qubit is owned by a unique process within a system.

Jorrand and Lalire [11,12,13,14] defined a language called QPAlg (Quantum Process Algebra), in which, based on CCS [2, 3], primitives of unitary transformations and quantum measurements were added to CCS. An operational semantics based on probabilistic branching bisimulation was given in QPAlg.

Ying et al. [15] was introduced as a kind of algebra of pure quantum processes (no classical data involved) based on CCS. qCCS aimed at providing a suitable framework, in which the mechanism of quantum concurrent computation can be understood, and interactions and conjugation of computation and communication in quantum systems can be observed. In qCCS, quantum operations (super operators) were chosen to describe transformations of quantum states, and quantum variables and their substitutions were carefully treated. An operational semantics for qCCS based on exact (strong) bisimulation and an approximation version of bisimulation were presented for qCCS.

Based on [15], several kind of bisimulations were presented for qCCS, such as probabilistic bisimulation [8], a kind of weak probabilistic bisimulation [17], open bisimulation [19] and symbolic bisimulation [16, 20]. These bisimulations provided qCSS with more semantic models. In some bisimulations, not only pure quantum data, but also classical data could be involved in qCCS.

In this paper, we propose an axiomatization of quantum processes called qACP, which is a quantum generalization of process algebra ACP. This work uses some results of the previous works, especially qCCS, in the following ways. (1) qACP still uses the concept of a quantum process configuration 〈p, ϱ〉 [8, 8,9,10,11,12, 15, 17, 20], which is usually consisted of a process term p and state information ϱ of all (public) quantum information variables. (2) Like qCCS, quantum operations are chosen to describe transformations of quantum states, and behave as the atomic actions of a pure quantum process. Quantum measurements are treated as quantum operations, so probabilistic bisimulations are avoided.

There are several innovations in this paper, we enumerate them as follows. (1) A weak bisimilarity (quantum branching bisimulation equivalence) is established for quantum processes. This weak bisimilarity is in a non-probabilistic way that follows [15] and can be used to model silent step and abstract internal actions. (2) We still use the framework of a quantum process configuration 〈p, ϱ〉, but we treat it as two relative independent part: the structural part p and the quantum part ϱ, because the establishment of a sound and complete theory is dependent on the structural properties of the structural part p. We let the quantum part ϱ be the outcomes of execution of p to examine and observe the function of the basic theory of quantum mechanics. We establish the relationship between quantum bisimilarity and classical bisimilarity, including strong bisimilarity and weak bisimilarity, which makes an axiomatization of quantum processes possible. (3) We establish a series of axiomatizations of quantum process algebra, including BQPA (Basic Quantum Process Algebra), QPAP (Quantum Process Algebra with Parallelism), AQCP (Algebra of Quantum Communicating Processes), AQCP with guarded linear recursion, and AQCP_τ with guarded linear recursion. Though these axiomatizations are based on classical axiomatizations of ACP which is based on the structural analysis the process p, they are not trivial and ordinary, because it is also necessary to examine if the outcomes ϱ of execution of p obey the basic quantum mechanics theory. For example, the associativity law of sequential composition ⋅, (x ⋅ y) ⋅ z = x ⋅ (y ⋅ z) (x, y, z range over the collection of process terms), is based on the associativity of quantum operations. And the behaviors of the silent step τ in quantum processes and that in classical processes are different under the framework of quantum process configuration 〈p, ϱ〉. (4) In this paper, qACP and classical ACP are unified under the framework of quantum process configuration 〈p, ϱ〉. This unifying means that quantum information and classical information can be mixed in qACP and quantum computing and classical computing are unified in qACP. Thus, qACP can be used widely for verification of quantum communication protocols, which involve not only quantum information, but also classical information. (5) As a result of axiomatization, qACP has not only an operational semantics, but also an equation logic which makes the qACP can be used easily. qACP also inherits the modularity of ACP, and can be extended in an elegant way.

3 Structural Operational Semantics Extended to Support Quantum Processes

In the above section, operational semantics are described by labelled transitions among process configurations, and a process term is enough to represent a process configuration. But in quantum processes, to avoid the abuse of quantum information which may violate the no-cloning theorem, a quantum process configuration 〈p, ϱ〉 [8,9,10,11,12, 15, 17, 20] is usually consisted of a process term p and state information ϱ of all (public) quantum information variables. Though quantum information variables are not explicitly defined in qACP and are hidden behind quantum operations, more importantly, the state information ϱ is the effects of execution of a series of quantum operations on involved quantum systems, the execution of a series of quantum operations should not only obey the restrictions of the structure of the process terms, but also those of quantum mechanics principles. Through the state information ϱ, we can check and observe the functions of quantum mechanics principles, such as quantum entanglement, quantum measurement, etc.

So, the operational semantics of quantum processes should be defined based on quantum process configuration 〈p, ϱ〉, in which ϱ = σ of two state information ϱ and σ means equality under the framework of quantum information and quantum computing, that is, these two quantum processes are in the same quantum state. Several important concepts used in this paper are following. Here, we use α, β to denote quantum operations in contrast to classical actions a, b.

Definition 3.1 (Quantum process configuration)

A quantum process configuration is defined to be a pair 〈p, ϱ〉, where p is a process (graph) called structural part of the configuration, and $\varrho \in \mathcal{D}\left(\mathcal{\mathscr{H}}\right)$ specifies the current state of the environment, which is called its quantum part.

Definition 3.2 (Quantum process graph)

A quantum process (graph) 〈p, ϱ〉 is an LTS in which one state s is elected to be the root. If the LTS contains a transition $s\overset{\alpha }{\rightarrow}{s}^{\prime }$, then $\left\langle p,\varrho \right\rangle \overset{\alpha }{\rightarrow}\left\langle {p}^{\prime },{\varrho}^{\prime}\right\rangle$ where 〈p^′, ϱ^′〉 has root state s^′. Moreover, if the LTS contains a transition sP, then 〈p, ϱ〉P. (1) A quantum process 〈p₀, ϱ₀〉 is finite if and only if the process p₀ is finite. (2) A quantum process 〈p₀, ϱ₀〉 is regular if and only if the process p₀ is regular.

Definition 3.3 (Quantum transition system specification)

A quantum process transition rule ϱ is an expression of the form $\frac{H}{\pi }$, with H a set of expressions $\left\langle t,\varrho \right\rangle \overset{\alpha }{\rightarrow}\left\langle {t}^{\prime },{\varrho}^{\prime}\right\rangle$ and 〈t, ϱ〉P with $t,{t}^{\prime}\in \mathbb{T}\left(\Sigma \right)$ and $\varrho, {\varrho}^{\prime}\in \mathcal{D}\left(\mathcal{\mathscr{H}}\right)$, called the (positive) premises of ϱ, and $t\overset{\alpha }{\rightarrow}{t}^{\prime }$, called structural part of H and denoted as H_s. And π an expression $\left\langle t,\varrho \right\rangle \overset{\alpha }{\rightarrow}\left\langle {t}^{\prime },{\varrho}^{\prime}\right\rangle$ or 〈t, ϱ〉P with $t,{t}^{\prime}\in \mathbb{T}\left(\Sigma \right)$ and $\varrho, {\varrho}^{\prime}\in \mathcal{D}\left(\mathcal{\mathscr{H}}\right)$, called the conclusion of ϱ, and $t\overset{\alpha }{\rightarrow}{t}^{\prime }$, called structural part of π and denoted as π_s. The left-hand side of π is called the source of ϱ. $\frac{H_s}{\pi_s}$ is called the structural part of ϱ and denoted as ϱ_s. A quantum process transition rule ϱ is closed if and only its structural part ϱ_s is closed. A quantum transition system specification (QTSS) is a (possible infinite) set of transition rules.

Definition 3.4 (Quantum bisimulation)

A bisimulation relation $\mathcal{B}$ is a binary relation on quantum processes such that: (1) if $\left\langle p,\varrho \right\rangle \mathcal{B} \left\langle q,\sigma \right\rangle$ and $\left\langle p,\varrho \right\rangle \overset{\alpha }{\rightarrow}\left\langle {p}^{\prime },{\varrho}^{\prime}\right\rangle$ then $\left\langle q,\sigma \right\rangle \overset{\alpha }{\rightarrow}\left\langle {q}^{\prime },{\sigma}^{\prime}\right\rangle$ with $\left\langle {p}^{\prime },{\varrho}^{\prime}\right\rangle \mathcal{B} \left\langle {q}^{\prime },{\sigma}^{\prime}\right\rangle$; (2) if $\left\langle p,\varrho \right\rangle \mathcal{B} \left\langle q,\sigma \right\rangle$ and $\left\langle q,\sigma \right\rangle \overset{\alpha }{\rightarrow}\left\langle {q}^{\prime },{\sigma}^{\prime}\right\rangle$ then $\left\langle p,\varrho \right\rangle \overset{\alpha }{\rightarrow}\left\langle {p}^{\prime },{\varrho}^{\prime}\right\rangle$ with $\left\langle {p}^{\prime },{\varrho}^{\prime}\right\rangle \mathcal{B} \left\langle {q}^{\prime },{\sigma}^{\prime}\right\rangle$; (3) if $\left\langle p,\varrho \right\rangle \mathcal{B} \left\langle q,\sigma \right\rangle$ and 〈p, ϱ〉P, then 〈q, σ〉P; (4) if $\left\langle p,\varrho \right\rangle \mathcal{B} \left\langle q,\sigma \right\rangle$ and 〈q, σ〉P, then 〈p, ϱ〉P. Two quantum process 〈p, ϱ〉 and 〈q, σ〉 are bisimilar, denoted by $\left\langle p,\varrho \right\rangle \underset{\_}{\leftrightarrow}\left\langle q,\sigma \right\rangle$, if there is a bisimulation relation $\mathcal{B}$ such that $\left\langle p,\varrho \right\rangle \mathcal{B} \left\langle q,\sigma \right\rangle$.

Definition 3.5 (Relation between quantum bisimulation and classical bisimulation)

For two quantum processes, $\left\langle p,\varrho \right\rangle \underset{\_}{\leftrightarrow}\left\langle q,\sigma \right\rangle$, with ϱ = σ, if and only if $p\underset{\_}{\leftrightarrow }q$ and ϱ^′ = σ^′, where ϱ evolves into ϱ^′ after execution of p and σ evolves into σ^′ after execution of q.

Definition 3.6 (Quantum branching bisimulation)

A branching bisimulation relation $\mathcal{B}$ is a binary relation on the collection of quantum processes such that: (1) if $\left\langle p,\varrho \right\rangle \mathcal{B} \left\langle q,\sigma \right\rangle$ and $\left\langle p,\varrho \right\rangle \overset{\alpha }{\rightarrow}\left\langle {p}^{\prime },{\varrho}^{\prime}\right\rangle$ then either α ≡ τ and $\left\langle {p}^{\prime },{\varrho}^{\prime}\right\rangle \mathcal{B} \left\langle q,\sigma \right\rangle$ or there is a sequence of (zero or more) τ-transitions $\left\langle q,\sigma \right\rangle \overset{\tau }{\rightarrow}\cdots \overset{\tau }{\rightarrow}\left\langle {q}_0,{\sigma}_0\right\rangle$ such that $\left\langle p,\varrho \right\rangle \mathcal{B} \left\langle {q}_0,{\sigma}_0\right\rangle$ and $\left\langle {q}_0,{\sigma}_0\right\rangle \overset{\alpha }{\rightarrow}\left\langle {q}^{\prime },{\sigma}^{\prime}\right\rangle$ with $\left\langle {p}^{\prime },{\varrho}^{\prime}\right\rangle \mathcal{B} \left\langle {q}^{\prime },{\sigma}^{\prime}\right\rangle$; (2) if $\left\langle p,\varrho \right\rangle \mathcal{B} \left\langle q,\sigma \right\rangle$ and $\left\langle q,\sigma \right\rangle \overset{\alpha }{\rightarrow}\left\langle {q}^{\prime },{\sigma}^{\prime}\right\rangle$ then either α ≡ τ and $\left\langle p,\varrho \right\rangle \mathcal{B} \left\langle {q}^{\prime },{\sigma}^{\prime}\right\rangle$ or there is a sequence of (zero or more) τ-transitions $\left\langle p,\varrho \right\rangle \overset{\tau }{\rightarrow}\cdots \overset{\tau }{\rightarrow}\left\langle {p}_0,{\varrho}_0\right\rangle$ such that $\left\langle {p}_0,{\varrho}_0\right\rangle \mathcal{B} \left\langle q,\sigma \right\rangle$ and $\left\langle {p}_0,{\varrho}_0\right\rangle \overset{\alpha }{\rightarrow}\left\langle {p}^{\prime },{\varrho}^{\prime}\right\rangle$ with $\left\langle {p}^{\prime },{\varrho}^{\prime}\right\rangle \mathcal{B} \left\langle {q}^{\prime },{\sigma}^{\prime}\right\rangle$; (3) if $\left\langle p,\varrho \right\rangle \mathcal{B} \left\langle q,\sigma \right\rangle$ and 〈p, ϱ〉P, then there is a sequence of (zero or more) τ-transitions $\left\langle q,\sigma \right\rangle \overset{\tau }{\rightarrow}\cdots \overset{\tau }{\rightarrow}\left\langle {q}_0,{\sigma}_0\right\rangle$ such that $\left\langle p,\varrho \right\rangle \mathcal{B} \left\langle {q}_0,{\sigma}_0\right\rangle$ and 〈q₀, σ₀〉P; (4) if $\left\langle p,\varrho \right\rangle \mathcal{B} \left\langle q,\sigma \right\rangle$ and 〈q, σ〉P, then there is a sequence of (zero or more) τ-transitions $\left\langle p,\varrho \right\rangle \overset{\tau }{\rightarrow}\cdots \overset{\tau }{\rightarrow}\left\langle {p}_0,{\varrho}_0\right\rangle$ such that $\left\langle {p}_0,{\varrho}_0\right\rangle \mathcal{B} \left\langle q,\sigma \right\rangle$ and 〈p₀, ϱ₀〉P. Two quantum processes 〈p, ϱ〉 and 〈q, σ〉 are branching bisimilar, denoted by $\left\langle p,\varrho \right\rangle {\underset{\_}{\leftrightarrow}}_b\left\langle q,\sigma \right\rangle$, if there is a branching bisimulation relation $\mathcal{B}$ such that $\left\langle p,\varrho \right\rangle \mathcal{B} \left\langle q,\sigma \right\rangle$.

Definition 3.7 (Relation between quantum branching bisimulation and classical branching bisimulation)

For two quantum processes, $\left\langle p,\varrho \right\rangle {\underset{\_}{\leftrightarrow}}_b\left\langle q,\sigma \right\rangle$, with ϱ = σ, if and only if $p{\underset{\_}{\leftrightarrow}}_bq$ and ϱ^′ = σ^′, where ϱ evolves into ϱ^′ after execution of p and σ evolves into σ^′ after execution of q.

Definition 3.8 (Quantum rooted branching bisimulation)

A rooted branching bisimulation relation $\mathcal{B}$ is a binary relation on quantum processes such that: (1) if $\left\langle p,\varrho \right\rangle \mathcal{B} \left\langle q,\sigma \right\rangle$ and $\left\langle p,\varrho \right\rangle \overset{\alpha }{\rightarrow}\left\langle {p}^{\prime },{\varrho}^{\prime}\right\rangle$ then $\left\langle q,\sigma \right\rangle \overset{\alpha }{\rightarrow}\left\langle {q}^{\prime },{\sigma}^{\prime}\right\rangle$ with $\left\langle {p}^{\prime },{\varrho}^{\prime}\right\rangle {\underset{\_}{\leftrightarrow}}_b\left\langle {q}^{\prime },{\sigma}^{\prime}\right\rangle$; (2) if $\left\langle p,\varrho \right\rangle \mathcal{B} \left\langle q,\sigma \right\rangle$ and $\left\langle q,\sigma \right\rangle \overset{\alpha }{\rightarrow}\left\langle {q}^{\prime },{\sigma}^{\prime}\right\rangle$ then $\left\langle p,\varrho \right\rangle \overset{\alpha }{\rightarrow}\left\langle {p}^{\prime },{\varrho}^{\prime}\right\rangle$ with $\left\langle {p}^{\prime },{\varrho}^{\prime}\right\rangle {\underset{\_}{\leftrightarrow}}_b\left\langle {q}^{\prime },{\sigma}^{\prime}\right\rangle$; (3) if $\left\langle p,\varrho \right\rangle \mathcal{B} \left\langle q,\sigma \right\rangle$ and 〈p, ϱ〉P, then 〈q, σ〉P; (4) if $\left\langle p,\varrho \right\rangle \mathcal{B} \left\langle q,\sigma \right\rangle$ and 〈q, σ〉P, then 〈p, ϱ〉P. Two quantum processes 〈p, ϱ〉 and 〈q, σ〉 are rooted branching bisimilar, denoted by $\left\langle p,\varrho \right\rangle {\underset{\_}{\leftrightarrow}}_{rb}\left\langle q,\sigma \right\rangle$, if there is a rooted branching bisimulation relation $\mathcal{B}$ such that $\left\langle p,\varrho \right\rangle \mathcal{B} \left\langle q,\sigma \right\rangle$.

Definition 3.9 (Relation between quantum rooted branching bisimulation and classical rooted branching bisimulation)

For two quantum processes, $\left\langle p,\varrho \right\rangle {\underset{\_}{\leftrightarrow}}_{rb}\left\langle q,\sigma \right\rangle$, with ϱ = σ, if and only if $p{\underset{\_}{\leftrightarrow}}_{rb}q$ and ϱ^′ = σ^′, where ϱ evolves into ϱ^′ after execution of p and σ evolves into σ^′ after execution of q.

Definition 3.10 (Congruence)

Let Σ be a signature and $\mathcal{D}\left(\mathcal{\mathscr{H}}\right)$ be the state space of the environment. An equivalence relation $\mathcal{B}$ on $\left\langle t\in \mathcal{T}\left(\Sigma \right),\varrho \in \mathcal{D}\left(\mathcal{\mathscr{H}}\right)\right\rangle$ is a congruence, i.e., for each f ∈Σ, if $\left\langle {s}_i,{\varrho}_i\right\rangle \mathcal{B} \left\langle {t}_i,{\sigma}_i\right\rangle$ for i ∈{1,⋯ ,ar(f)}, then $f\left(\left\langle {s}_1,{\varrho}_1\right\rangle, \cdots \kern0.3em ,\left\langle {s}_{\mathrm{ar}(f)},{\varrho}_{\mathrm{ar}(f)}\right\rangle \right)\mathcal{B} \mathcal{f}\left(\left\langle {t}_1,{\sigma}_1\right\rangle, \cdots \kern0.3em ,\right\langle {t}_{\mathrm{ar}(f)},{\sigma}_{\mathrm{ar}(f)}\Big)$. An equivalence relation $\mathcal{B}$ on $\left\langle t\in \mathcal{T}\left(\Sigma \right),\varrho \in \mathcal{D}\left(\mathcal{\mathscr{H}}\right)\right\rangle$ is a congruence, if for each f ∈Σ, ${s}_i\mathcal{B} {t}_i$ for i ∈{1,⋯ ,ar(f)}, and $f\left({s}_1,\cdots \kern0.3em ,{s}_{\mathrm{ar}(f)}\right)\mathcal{B} \mathcal{f}\left({t}_1,\cdots \kern0.3em ,{t}_{\mathrm{ar}(f)}\right)$.

Definition 3.11 (Quantum conservative extension)

Let T₀ and T₁ be QTSSs over signature Σ₀ and $\mathcal{D}\left({\mathcal{\mathscr{H}}}_0\right)$, and Σ₁ and $\mathcal{D}\left({\mathcal{\mathscr{H}}}_1\right)$, respectively. The QTSS T₀ ⊕ T₁ is a conservative extension of T₀ if the LTSs generated by T₀ and T₀ ⊕ T₁ contain exactly the same transitions $\left\langle t,\varrho \right\rangle \overset{\alpha }{\rightarrow}\left\langle {t}^{\prime },{\varrho}^{\prime}\right\rangle$ and 〈t, ϱ〉P with $t\in \mathcal{T}\left({\Sigma}_0\right)$ and $\varrho \in \mathcal{D}\left({\mathcal{\mathscr{H}}}_0\right)$, and ${T}_0\oplus {T}_1=\left\langle {\Sigma}_0\cup {\Sigma}_1,\mathcal{D}\left({\mathcal{\mathscr{H}}}_0\otimes {\mathcal{\mathscr{H}}}_1\right)\right\rangle$.

Definition 3.12 (Relation between quantum conservative extension and classical conservative extension)

The QTSS T₀ ⊕ T₁ is a quantum conservative extension of T₀ with transitions $\left\langle t,\varrho \right\rangle \overset{\alpha }{\rightarrow}\left\langle {t}^{\prime },{\varrho}^{\prime}\right\rangle$ and 〈t, ϱ〉P, if its corresponding TSS ${T}_0^{\prime}\oplus {T}_1^{\prime }$ is a conservative extension of ${T}_0^{\prime }$ with transitions $t\overset{\alpha }{\rightarrow}{t}^{\prime }$ and tP.

4 BQPA – Basic Quantum Process Algebra

In the following, the variables x, x^′, y, y^′, z, z^′ range over the collection of process terms, the variables υ, ω range over the set A of atomic quantum operations, α, β ∈ A, s, s^′, t, t^′ are closed items, τ is the special constant silent step, δ is the special constant deadlock, and the predicate $\overset{\alpha }{\rightarrow}\surd$ represents successful termination after execution of the quantum operation α.

BQPA includes three kind of operators: the execution of atomic quantum operation α, the alternative composition operator + and the sequential composition operator ⋅. Each finite process can be represented by a closed term that is built from the set A of atomic quantum operations, the alternative composition operator + , and the sequential composition operator ⋅. The collection of all basic process terms is called Basic Quantum Process Algebra (BQPA), which is abbreviated to BQPA.

4.1 Transition Rules of BQPA

We give the transition rules under quantum transition system specification (QTSS) for BQPA as follows.

$$ \frac{}{\left\langle \upsilon, \varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle \surd, \upsilon \left(\varrho \right)\right\rangle } $$

$$ \frac{\left\langle x,\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle \surd, {\varrho}^{\prime}\right\rangle }{\left\langle x+y,\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle \surd, {\varrho}^{\prime}\right\rangle } $$

$$ \frac{\left\langle x,\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle {x}^{\prime },{\varrho}^{\prime}\right\rangle }{\left\langle x+y,\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle {x}^{\prime },{\varrho}^{\prime}\right\rangle } $$

$$ \frac{\left\langle y,\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle \surd, {\varrho}^{\prime}\right\rangle }{\left\langle x+y,\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle \surd, {\varrho}^{\prime}\right\rangle } $$

$$ \frac{\left\langle y,\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle {y}^{\prime },{\varrho}^{\prime}\right\rangle }{\left\langle x+y,\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle {y}^{\prime },{\varrho}^{\prime}\right\rangle } $$

$$ \frac{\left\langle x,\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle \surd, {\varrho}^{\prime}\right\rangle }{\left\langle x\cdot y,\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle y,{\varrho}^{\prime}\right\rangle } $$

$$ \frac{\left\langle x,\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle {x}^{\prime },{\varrho}^{\prime}\right\rangle }{\left\langle x\cdot y,\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle {x}^{\prime}\cdot y,{\varrho}^{\prime}\right\rangle } $$

where υ(ϱ) represents the new state of a quantum system, whose origin state is ϱ, after the execution of the atomic quantum operation υ.

• The first transition rule says that each atomic quantum operation υ can terminate successfully, and the state of the environment would be changed from ϱ to υ(ϱ).

• The next four transition rules say that s + t can execute alternatively, that is, it can execute either s or t.

• The last two transition rules say that s ⋅ t can execute sequentially, that is, it executes s in the first, after successful termination of s, then execution of t follows.

4.2 Axiomatization for BQPA

We design an axiomatization ${\mathcal{E}}_{\mathrm{BQPA}}$ for BQPA modulo quantum bisimulation equivalence as Table 1 shows.

Table 1 Axioms for BQPA

Several important conclusions are following.

Theorem 4.1

Quantum bisimulation equivalence is a congruence with respect to BQPA.

Proof

The structural part of QTSSs for BQPA are all in panth format, so bisimulation equivalence that they induce is a congruence. According to the definition of quantum bisimulation, quantum bisimulation equivalence that QTSSs for BQPA induce is also a congruence. □

Theorem 4.2

${\mathcal{E}}_{\mathrm{BQPA}}$ is sound for BQPA modulo quantum bisimulation equivalence.

Proof

Since quantum bisimulation is both an equivalence and a congruence for BQPA, only the soundness of the first clause in the definition of the relation = is needed to be checked. That is, if s = t is an axiom in ${\mathcal{E}}_{\mathrm{BQPA}}$ and σ a closed substitution that maps the variable in s and t to basic quantum process terms, then we need to check that $\left\langle \sigma (s),\varrho \right\rangle \underset{\_}{\leftrightarrow}\left\langle \sigma (t),\sigma \right\rangle$.

Since axioms in ${\mathcal{E}}_{\mathrm{BQPA}}$ (same as ${\mathcal{E}}_{\mathrm{BPA}}$) are sound for BPA modulo bisimulation equivalence, according to the definition of quantum bisimulation, we only need to check if ϱ^′ = σ^′, where ϱ evolves into ϱ^′ after execution of σ(s) and σ evolves into σ^′ after execution of σ(t). For example, the axiom QA5 is sound for BQPA modulo quantum bisimulation equivalence, based on the associativity of quantum operations, that is, (σ(s) ⋅ σ(t)) ⋅ σ(u)(ϱ) = σ(s) ⋅ (σ(t) ⋅ σ(u))(σ) for any ϱ = σ. □

Theorem 4.3

${\mathcal{E}}_{\mathrm{BQPA}}$ is complete for BQPA modulo quantum bisimulation equivalence.

Proof

To prove that ${\mathcal{E}}_{\mathrm{BQPA}}$ is complete for BQPA modulo quantum bisilumation equivalence, it means that $\left\langle s,\varrho \right\rangle \underset{\_}{\leftrightarrow}\left\langle t,\sigma \right\rangle$ implies s = t.

It was already proved that ${\mathcal{E}}_{\mathrm{BQPA}}$ (same as ${\mathcal{E}}_{\mathrm{BPA}}$) is complete for BPA modulo bisimulation equivalence, that is, $s\underset{\_}{\leftrightarrow }t$ implies s = t. $\left\langle s,\varrho \right\rangle \underset{\_}{\leftrightarrow}\left\langle t,\sigma \right\rangle$ with ϱ = σ means that $s\underset{\_}{\leftrightarrow }t$ with ϱ = σ and ϱ^′ = σ^′, where ϱ evolves into ϱ^′ after execution of s and σ evolves into σ^′ after execution of t, according to the definition of quantum bisimulation equivalence. The completeness of ${\mathcal{E}}_{\mathrm{BQPA}}$ for BPA modulo bisimulation equivalence determines that ${\mathcal{E}}_{\mathrm{BQPA}}$ is complete for BQPA modulo quantum bisimulation equivalence. □

5 AQCP – Algebra of Quantum Communicating Processes

It is well known that process algebra captures parallelism and concurrency by means of the so-called interleaving pattern in contrast to the so-called true concurrency. Quantum processes can execute in parallel and communicate with each other, since the actions used to communicate are not quantum operations, which means that after the execution of communicating actions, the quantum state maintains unchanged. We introduce a new set C of atomic communicating actions. A merge operator ∥ and a communication function γ : C × C → C can be used to capture the parallelism and the communication.

In the following, the variables υ, ω range over the set A of atomic quantum operations, and the variable ν, μrange over the set C of atomic communicating actions.

The merge 〈s ∥ t, ϱ〉 can choose to execute an initial transition of process term s or an initial transition of process term t, and change the quantum state, which is captured by the following four transition rules.

$$ \frac{\left\langle x,\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle \surd, {\varrho}^{\prime}\right\rangle }{\left\langle x\parallel y,\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle y,{\varrho}^{\prime}\right\rangle } $$

$$ \frac{\left\langle x,\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle {x}^{\prime },{\varrho}^{\prime}\right\rangle }{\left\langle x\parallel y,\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle {x}^{\prime}\parallel y,{\varrho}^{\prime}\right\rangle } $$

$$ \frac{\left\langle y,\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle \surd, {\varrho}^{\prime}\right\rangle }{\left\langle x\parallel y,\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle x,{\varrho}^{\prime}\right\rangle } $$

$$ \frac{\left\langle y,\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle {y}^{\prime },{\varrho}^{\prime}\right\rangle }{\left\langle x\parallel y,\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle x\parallel {y}^{\prime },{\varrho}^{\prime}\right\rangle } $$

And also the merge 〈s ∥ t, ϱ〉 can choose to execute a communication of initial transitions of the process term s and t, and does not change the quantum state, which is expressed by the following four transition rules.

$$ \frac{\left\langle x,\varrho \right\rangle \overset{\nu }{\rightarrow}\left\langle \surd, \varrho \right\rangle \kern1em \left\langle y,\varrho \right\rangle \overset{\mu }{\rightarrow}\left\langle \surd, \varrho \right\rangle }{\left\langle x\parallel y,\varrho \right\rangle \overset{\gamma \left(\nu, \mu \right)}{\rightarrow}\left\langle \surd, \varrho \right\rangle } $$

$$ \frac{\left\langle x,\varrho \right\rangle \overset{\nu }{\rightarrow}\left\langle \surd, \varrho \right\rangle \kern1em \left\langle y,\varrho \right\rangle \overset{\mu }{\rightarrow}\left\langle {y}^{\prime },\varrho \right\rangle }{\left\langle x\parallel y,\varrho \right\rangle \overset{\gamma \left(\nu, \mu \right)}{\rightarrow}\left\langle {y}^{\prime },\varrho \right\rangle } $$

$$ \frac{\left\langle x,\varrho \right\rangle \overset{\nu }{\rightarrow}\left\langle {x}^{\prime },\varrho \right\rangle \kern1em \left\langle y,\varrho \right\rangle \overset{\mu }{\rightarrow}\left\langle \surd, \varrho \right\rangle }{\left\langle x\parallel y,\varrho \right\rangle \overset{\gamma \left(\nu, \mu \right)}{\rightarrow}\left\langle {x}^{\prime },\varrho \right\rangle } $$

$$ \frac{\left\langle x,\varrho \right\rangle \overset{\nu }{\rightarrow}\left\langle {x}^{\prime },\varrho \right\rangle \kern1em \left\langle y,\varrho \right\rangle \overset{\mu }{\rightarrow}\left\langle {y}^{\prime },\varrho \right\rangle }{\left\langle x\parallel y,\varrho \right\rangle \overset{\gamma \left(\nu, \mu \right)}{\rightarrow}\left\langle {x}^{\prime}\parallel {y}^{\prime },\varrho \right\rangle } $$

5.1 Left Merge and Communication Merge

Since there does not exist a sound and complete finite axiomatization for BPA extended with the merge, modulo bisimulation equivalence, it is can be proved that there does not exist a sound and complete axiomatization for BQPA extended with the merge modulo quantum bisimulation equivalence either. This can be overcome by defining two extra operator that are called left merge and communication merge ∣. We call BQPA extended with the merge operator ∥, the left merge operator and the communication merge operator ∣ as Quantum Process Algebra with Parallelism, which is abbreviated to QPAP.

5.1.1 Transition Rules of QPAP

The left merge takes its initial transition from the process term s and changes the quantum state, and then behaves as the merge ∥, which is expressed by the following two transition rules.

The communication merge 〈s∣t, ϱ〉 executes as initial transition a communication between initial transition of the process term s and t, and does not change the quantum state, and then behaves as the merge operator ∥, which is captured by the following four transition rules.

$$ \frac{\left\langle x,\varrho \right\rangle \overset{\nu }{\rightarrow}\left\langle \surd, \varrho \right\rangle \kern1em \left\langle y,\varrho \right\rangle \overset{\mu }{\rightarrow}\left\langle \surd, \varrho \right\rangle }{\left\langle x\mid y,\varrho \right\rangle \overset{\gamma \left(\nu, \mu \right)}{\rightarrow}\left\langle \surd, \varrho \right\rangle } $$

$$ \frac{\left\langle x,\varrho \right\rangle \overset{\nu }{\rightarrow}\left\langle \surd, \varrho \right\rangle \kern1em \left\langle y,\varrho \right\rangle \overset{\mu }{\rightarrow}\left\langle {y}^{\prime },\varrho \right\rangle }{\left\langle x\mid y,\varrho \right\rangle \overset{\gamma \left(\nu, \mu \right)}{\rightarrow}\left\langle {y}^{\prime },\varrho \right\rangle } $$

$$ \frac{\left\langle x,\varrho \right\rangle \overset{\nu }{\rightarrow}\left\langle {x}^{\prime },\varrho \right\rangle \kern1em \left\langle y,\varrho \right\rangle \overset{\mu }{\rightarrow}\left\langle \surd, \varrho \right\rangle }{\left\langle x\mid y,\varrho \right\rangle \overset{\gamma \left(\nu, \mu \right)}{\rightarrow}\left\langle {x}^{\prime },\varrho \right\rangle } $$

$$ \frac{\left\langle x,\varrho \right\rangle \overset{\nu }{\rightarrow}\left\langle {x}^{\prime },\varrho \right\rangle \kern1em \left\langle y,\varrho \right\rangle \overset{\mu }{\rightarrow}\left\langle {y}^{\prime },\varrho \right\rangle }{\left\langle x\mid y,\varrho \right\rangle \overset{\gamma \left(\nu, \mu \right)}{\rightarrow}\left\langle {x}^{\prime}\parallel {y}^{\prime },\varrho \right\rangle } $$

It must be pointed out that the communication function γ(ν, μ) of two communicating actions ν and μ is used to exchange data between two interleaving quantum processes. Due to the quantum no-cloning theorem, the data must be exchanged by references (the names of the quantum variables), but not by values.

Theorem 5.1

QPAP is a conservative extension of BQPA.

Proof

Since the corresponding TSS of BQPA is source-dependent, and the transition rules for merge operator ∥, left merge operator and communication merge ∣ contain only a fresh operator in their source, so the corresponding TSS of QPAP is a conservative extension of that of BQPA. That means that QPAP is a conservative extension of BQPA. □

Theorem 5.2

Quantum bisimulation equivalence is a congruence with respect to QPAP.

Proof

The structural part of QTSSs for QPAP and BQPA are all in panth format, so bisimulation equivalence that they induce is a congruence. According to the definition of quantum bisimulation, quantum bisimulation equivalence that QTSSs for QPAP induce is also a congruence. □

5.1.2 Axiomatization for QPAP

We design an axiomatization for QPAP illustrated in Table 2.

Table 2 Axioms for QPAP

Then, we can get the soundness and completeness theorems as follows.

Theorem 5.3

${\mathcal{E}}_{\mathrm{QPAP}}$ is sound for QPAP modulo quantum bisimulation equivalence.

Proof

Since quantum bisimulation is both an equivalence and a congruence for QPAP, only the soundness of the first clause in the definition of the relation = is needed to be checked. That is, if s = t is an axiom in ${\mathcal{E}}_{\mathrm{QPAP}}$ and σ a closed substitution that maps the variable in s and t to basic quantum process terms, then we need to check that $\left\langle \sigma (s),\varrho \right\rangle \underset{\_}{\leftrightarrow}\left\langle \sigma (t),\sigma \right\rangle$.

Since axioms in ${\mathcal{E}}_{\mathrm{QPAP}}$ (same as ${\mathcal{E}}_{\mathrm{PAP}}$) are sound for PAP modulo bisimulation equivalence, according to the definition of quantum bisimulation, we only need to check if ϱ^′ = σ^′ when ϱ = σ, where ϱ evolves into ϱ^′ after execution of σ(s) and σ evolves into σ^′ after execution of σ(t). We can find that every axiom in Table 2 meets the above condition. □

Theorem 5.4

${\mathcal{E}}_{\mathrm{QPAP}}$ is complete for QPAP modulo quantum bisimulation equivalence.

Proof

To prove that ${\mathcal{E}}_{\mathrm{QPAP}}$ is complete for QPAP modulo quantum bisilumation equivalence, it means that $\left\langle s,\varrho \right\rangle \underset{\_}{\leftrightarrow}\left\langle t,\sigma \right\rangle$ implies s = t.

It was already proved that ${\mathcal{E}}_{\mathrm{QPAP}}$ (same as ${\mathcal{E}}_{\mathrm{PAP}}$) is complete for PAP modulo bisimulation equivalence, that is, $s\underset{\_}{\leftrightarrow }t$ implies s = t. $\left\langle s,\varrho \right\rangle \underset{\_}{\leftrightarrow}\left\langle t,\sigma \right\rangle$ with ϱ = σ means that $s\underset{\_}{\leftrightarrow }t$ with ϱ = σ and ϱ^′ = σ^′, where ϱ evolves into ϱ^′ after execution of s and σ evolves into σ^′ after execution of t, according to the definition of quantum bisimulation equivalence. The completeness of ${\mathcal{E}}_{\mathrm{QPAP}}$ for PAP modulo bisimulation equivalence determines that ${\mathcal{E}}_{\mathrm{QPAP}}$ is complete for QPAP modulo quantum bisimulation equivalence. □

5.2 Deadlock and Encapsulation

The mismatch of two communicating action pair ν and μ can cause a deadlock (nothing to do), we introduce the deadlock constant δ and extend the communication function γ to γ : C × C → C ∪{δ}. So, the introduction about communication merge ∣ in the above section should be with γ(ν, μ)≠δ. We also introduce a unary encapsulation operator ∂_H for sets H of atomic communicating actions, which rename all actions in H into δ. QPAP extended with deadlock constant δ and encapsulation operator ∂_H is called the Algebra of Quantum Communicating Processes, which is abbreviated to AQCP.

5.2.1 Transition Rules of AQCP

The encapsulation operator ∂_H(t) can execute all transitions of process term t of which the labels are not in H, and does not change the quantum state, which is expressed by the following two transition rules.

$$ \frac{\left\langle x,\varrho \right\rangle \overset{\nu }{\rightarrow}\left\langle \surd, \varrho \right\rangle }{\left\langle {\partial}_H(x),\varrho \right\rangle \overset{\nu }{\rightarrow}\left\langle \surd, \varrho \right\rangle}\kern2.00em \nu \notin H $$

$$ \frac{\left\langle x,\varrho \right\rangle \overset{\nu }{\rightarrow}\left\langle {x}^{\prime },\varrho \right\rangle }{\left\langle {\partial}_H(x),\varrho \right\rangle \overset{\nu }{\rightarrow}\left\langle {\partial}_H\left({x}^{\prime}\right),\varrho \right\rangle}\kern2.00em \nu \notin H $$

Theorem 5.5

AQCP is a conservative extension of QPAP.

Proof

Since the corresponding TSS of QPAP is source-dependent, and the transition rules for encapsulation operator ∂_H contain only a fresh operator in their source, so the corresponding TSS of AQCP is a conservative extension of that of QPAP. That means that AQCP is a conservative extension of QPAP. □

Theorem 5.6

Quantum bisimulation equivalence is a congruence with respect to AQCP.

Proof

The structural part of QTSSs for AQCP and QPAP are all in panth format, so bisimulation equivalence that they induce is a congruence. According to the definition of quantum bisimulation, quantum bisimulation equivalence that QTSSs for AQCP induce is also a congruence. □

5.2.2 Axiomatization for AQCP

The axioms for AQCP are shown in Table 3.

Table 3 Axioms for AQCP

The soundness and completeness theorems are following.

Theorem 5.7

${\mathcal{E}}_{\mathrm{AQCP}}$ is sound for AQCP modulo quantum bisimulation equivalence.

Proof

Since quantum bisimulation is both an equivalence and a congruence for AQCP, only the soundness of the first clause in the definition of the relation = is needed to be checked. That is, if s = t is an axiom in ${\mathcal{E}}_{\mathrm{AQCP}}$ and σ a closed substitution that maps the variable in s and t to basic quantum process terms, then we need to check that $\left\langle \sigma (s),\varrho \right\rangle \underset{\_}{\leftrightarrow}\left\langle \sigma (t),\sigma \right\rangle$.

Since axioms in ${\mathcal{E}}_{\mathrm{AQCP}}$ (same as ${\mathcal{E}}_{\mathrm{ACP}}$) are sound for ACP modulo bisimulation equivalence, according to the definition of quantum bisimulation, we only need to check if ϱ^′ = σ^′ when ϱ = σ, where ϱ evolves into ϱ^′ after execution of σ(s) and σ evolves into σ^′ after execution of σ(t). We can find that every axiom in Table 3 meets the above condition. □

Theorem 5.8

${\mathcal{E}}_{\mathrm{AQCP}}$ is complete for AQCP modulo quantum bisimulation equivalence.

Proof

To prove that ${\mathcal{E}}_{\mathrm{AQCP}}$ is complete for AQCP modulo quantum bisilumation equivalence, it means that $\left\langle s,\varrho \right\rangle \underset{\_}{\leftrightarrow}\left\langle t,\sigma \right\rangle$ implies s = t.

It was already proved that ${\mathcal{E}}_{\mathrm{AQCP}}$ (same as ${\mathcal{E}}_{\mathrm{ACP}}$) is complete for ACP modulo bisimulation equivalence, that is, $s\underset{\_}{\leftrightarrow }t$ implies s = t. $\left\langle s,\varrho \right\rangle \underset{\_}{\leftrightarrow}\left\langle t,\sigma \right\rangle$ with ϱ = σ means that $s\underset{\_}{\leftrightarrow }t$ with ϱ = σ and ϱ^′ = σ^′, where ϱ evolves into ϱ^′ after execution of s and σ evolves into σ^′ after execution of t, according to the definition of quantum bisimulation equivalence. The completeness of ${\mathcal{E}}_{\mathrm{AQCP}}$ for ACP modulo bisimulation equivalence determines that ${\mathcal{E}}_{\mathrm{AQCP}}$ is complete for AQCP modulo quantum bisimulation equivalence. □

6 Recursion

To capture infinite computing, recursion is introduced in this section. In the following, E, F, G are guarded linear recursion specifications, X, Y, Z are recursive variables. We first introduce several important concepts, which come from [5].

Definition 6.1 (Recursive specification)

A recursive specification is a finite set of recursive equations

$$ {X}_1={t}_1\left({X}_1,\cdots \kern0.3em ,{X}_n\right) $$

$$ ... $$

$$ {X}_n={t}_n\left({X}_1,\cdots \kern0.3em ,{X}_n\right) $$

where the left-hand sides of X_i are called recursion variables, and the right-hand sides t_i(X₁,⋯ ,X_n) are process terms in AQCP with possible occurrences of the recursion variables X₁,⋯ ,X_n.

Definition 6.2 (Solution)

Processes p₁,⋯ ,p_n are a solution for a recursive specification {X_i = t_i(X₁,⋯ ,X_n)|i ∈{1,⋯ ,n}} (with respect to bisimulation equivalence) if ${p}_i\underset{\_}{\leftrightarrow }{t}_i\left({p}_1,\cdots \kern0.3em ,{p}_n\right)$ for i ∈{1,⋯ ,n}.

Definition 6.3 (Guarded recursive specification)

A recursive specification

$$ {X}_1={t}_1\left({X}_1,\cdots \kern0.3em ,{X}_n\right) $$

$$ ... $$

$$ {X}_n={t}_n\left({X}_1,\cdots \kern0.3em ,{X}_n\right) $$

is guarded if the right-hand sides of its recursive equations can be adapted to the form by applications of the axioms in ${\mathcal{E}}_{\mathrm{AQCP}}$ and replacing recursion variables by the right-hand sides of their recursive equations,

$$ {\alpha}_1\cdot {s}_1\left({X}_1,\cdots \kern0.3em ,{X}_n\right)+\cdots +{\alpha}_k\cdot {s}_k\left({X}_1,\cdots \kern0.3em ,{X}_n\right)+{\beta}_1+\cdots +{\beta}_l $$

where α₁,⋯ ,α_k, β₁,⋯ ,β_l ∈ A ∪ C, and the sum above is allowed to be empty, in which case it represents the deadlock δ.

Definition 6.4 (Linear recursive specification)

A recursive specification is linear if its recursive equations are of the form

$$ {\alpha}_1{X}_1+\cdots +{\alpha}_k{X}_k+{\beta}_1+\cdots +{\beta}_l $$

where α₁,⋯ ,α_k, β₁,⋯ ,β_l ∈ A ∪ C, and the sum above is allowed to be empty, in which case it represents the deadlock δ.

6.1 Transition Rules of Guarded Recursion

For a guarded recursive specifications E with the form

$$ {X}_1={t}_1\left({X}_1,\cdots \kern0.3em ,{X}_n\right) $$

$$ \cdots $$

$$ {X}_n={t}_n\left({X}_1,\cdots \kern0.3em ,{X}_n\right) $$

the behavior of the solution 〈X_i|E〉 for the recursion variable X_i in E, where i ∈{1,⋯ ,n}, is exactly the behavior of their right-hand sides t_i(X₁,⋯ ,X_n), which is captured by the following two transition rules.

$$ \frac{\left\langle {t}_i\left(\left\langle {X}_1|E\right\rangle, \cdots \kern0.3em ,\left\langle {X}_n|E\right\rangle \right),\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle \surd, {\varrho}^{\prime}\right\rangle }{\left\langle \left\langle {X}_i|E\right\rangle, \varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle \surd, {\varrho}^{\prime}\right\rangle } $$

$$ \frac{\left\langle {t}_i\left(\left\langle {X}_1|E\right\rangle, \cdots \kern0.3em ,\left\langle {X}_n|E\right\rangle \right),\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle y,{\varrho}^{\prime}\right\rangle }{\left\langle \left\langle {X}_i|E\right\rangle, \varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle y,{\varrho}^{\prime}\right\rangle } $$

Theorem 6.1

AQCP with guarded recursion is a conservative extension of AQCP.

Proof

Since the corresponding TSS of AQCP is source-dependent, and the transition rules for guarded recursion contain only a fresh constant in their source, so the corresponding TSS of AQCP with guarded recursion is a conservative extension of that of AQCP. That means that AQCP with guarded recursion is a conservative extension of AQCP. □

Theorem 6.2

Quantum bisimulation equivalence is a congruence with respect to AQCP with guarded recursion.

Proof

The structural part of QTSSs for guarded recursion and AQCP are all in panth format, so bisimulation equivalence that they induce is a congruence. According to the definition of quantum bisimulation, quantum bisimulation equivalence that QTSSs for AQCP with guarded recursion induce is also a congruence. □

6.2 Axiomatization for Guarded Recursion

The RDP (Recursive Definition Principle) and the RSP (Recursive Specification Principle) are shown in Table 4.

Table 4 Recursive definition principle and recursive specification principle

Theorem 6.3

${\mathcal{E}}_{\mathrm{AQCP}}$ + RDP + RSP is sound for AQCP with guarded recursion modulo quantum bisimulation equivalence.

Proof

Since quantum bisimulation is both an equivalence and a congruence for AQCP with guarded recursion, only the soundness of the first clause in the definition of the relation = is needed to be checked. That is, if s = t is an axiom in ${\mathcal{E}}_{\mathrm{AQCP}}$ + RDP + RSP and σ a closed substitution that maps the variable in s and t to basic quantum process terms, then we need to check that $\left\langle \sigma (s),\varrho \right\rangle \underset{\_}{\leftrightarrow}\left\langle \sigma (t),\sigma \right\rangle$.

Since axioms in ${\mathcal{E}}_{\mathrm{AQCP}}$ + RDP + RSP (same as ${\mathcal{E}}_{\mathrm{ACP}}$ + RDP + RSP) are sound for ACP with guarded recursion modulo bisimulation equivalence, according to the definition of quantum bisimulation, we only need to check if ϱ^′ = σ^′ when ϱ = σ, where ϱ evolves into ϱ^′ after execution of σ(s) and σ evolves into σ^′ after execution of σ(t). We can find that every axiom in Table 4 meets the above condition. □

Theorem 6.4

${\mathcal{E}}_{\mathrm{AQCP}}$ + RDP + RSP is complete for AQCP with linear recursion modulo quantum bisimulation equivalence.

Proof

To prove that ${\mathcal{E}}_{\mathrm{AQCP}}$ + RDP + RSP is complete for AQCP with linear recursion modulo quantum bisilumation equivalence, it means that $\left\langle s,\varrho \right\rangle \underset{\_}{\leftrightarrow}\left\langle t,\sigma \right\rangle$ implies s = t.

It was already proved that ${\mathcal{E}}_{\mathrm{AQCP}}$ + RDP + RSP (same as ${\mathcal{E}}_{\mathrm{ACP}}$ + RDP +RSP) is complete for ACP with linear recursion modulo bisimulation equivalence, that is, $s\underset{\_}{\leftrightarrow }t$ implies s = t. $\left\langle s,\varrho \right\rangle \underset{\_}{\leftrightarrow}\left\langle t,\sigma \right\rangle$ with ϱ = σ means that $s\underset{\_}{\leftrightarrow }t$ with ϱ = σ and ϱ^′ = σ^′, where ϱ evolves into ϱ^′ after execution of s and σ evolves into σ^′ after execution of t, according to the definition of quantum bisimulation equivalence. The completeness of ${\mathcal{E}}_{\mathrm{AQCP}}$ + RDP + RSP for ACP with linear recursion modulo bisimulation equivalence determines that ${\mathcal{E}}_{\mathrm{AQCP}}$ + RDP + RSP is complete for AQCP with linear recursion modulo quantum bisimulation equivalence. □

7 Abstraction

A quantum program has internal implementations and external behaviors. Abstraction technology abstracts away from the internal steps to check if the internal implementations really display the desired external behaviors. This makes the introduction of special silent step constant τ and the abstraction operator τ_I.

Firstly, we introduce the concept of guarded linear recursive specification, which comes from [5].

Definition 7.1 (Guarded linear recursive specification)

A recursive specification is linear if its recursive equations are of the form

$$ {\alpha}_1{X}_1+\cdots +{\alpha}_k{X}_k+{\beta}_1+\cdots +{\beta}_l $$

where α₁,⋯ ,α_k, β₁,⋯ ,β_l ∈ A ∪ C ∪{τ}.

A linear recursive specification E is guarded if there does not exist an infinite sequence of τ-transitions $\left\langle X|E\right\rangle \overset{\tau }{\rightarrow}\left\langle {X}^{\prime }|E\right\rangle \overset{\tau }{\rightarrow}\left\langle {X}^{\prime \prime }|E\right\rangle \overset{\tau }{\rightarrow}\cdots \kern0.3em$.

7.1 Silent Step

A τ-transition is silent, which is means that it can be eliminated from a quantum process graph. τ is an internal step and keep silent from an external observer, but please remember, τ is a quantum operation in nature. This fact makes that τ must influence the state of all quantum variables ϱ, that is, τ is not really silent for a quantum process configuration 〈p, ϱ〉. To make τ keep silent, the definition of ϱ must be changed, that is, ϱ does not record the state of all quantum variables, some variables must be moved away. But, what variables should be moved away? The quantum variables that τ may influence are called private variables. These private variables include not only the variables τ directly manipulates, but also those variables which are entangled with the variables that τ directly manipulates. The quantum variables that τ can not influence are called public variables. In the following, ϱ records the state of all public variables. We use the symbol τ(ϱ) to denote the state of all public quantum variables after execution of τ. From an external view, we can see that ϱ = τ(ϱ).

The processing of τ in quantum processes is some what farfetched. But, it is the only choice under the framework of quantum process configuration 〈p, ϱ〉. Otherwise, the concept of branching bisimulation (weak bisimilarity) and the theory of abstraction can not be established.

Now, the set A of all quantum operations is extended to A ∪{τ}, C to C ∪{τ}, and γ to γ : C ∪{τ}× C ∪{τ}→ C ∪{δ}.

7.1.1 Transition Rules of Silent Step

τ keeps silent from an external observer, which is expressed by the following transition rules.

$$ \frac{}{\left\langle \tau, \varrho \right\rangle \overset{\tau }{\rightarrow}\left\langle \surd, \tau \left(\varrho \right)\right\rangle } $$

Transition rules for alternative composition, sequential composition and guarded linear recursion that involves τ-transitions are omitted.

Theorem 7.1

AQCP with silent step and guarded linear recursion is a conservative extension of AQCP with guarded linear recursion.

Proof

The corresponding TSS of AQCP with silent step and guarded linear recursion is a conservative extension of that of AQCP with guarded linear recursion. That means that AQCP with silent step and guarded linear recursion is a conservative extension of AQCP with guarded linear recursion. □

Theorem 7.2

Quantum rooted branching bisimulation equivalence is a congruence with respect to AQCP with silent step and guarded linear recursion.

Proof

The structural part of QTSSs for AQCP with silent step and guarded linear recursion are all in RBB cool format by incorporating the successful termination predicate ↓ in the transition rules, so rooted branching bisimulation equivalence that they induce is a congruence. According to the definition of quantum rooted branching bisimulation, quantum rooted branching bisimulation equivalence that QTSSs for AQCP with silent step and guarded linear recursion induce is also a congruence.□

7.1.2 Axioms for Silent Step

The axioms for silent step is shown in Table 5.

Table 5 Axioms for silent step

Theorem 7.3

${\mathcal{E}}_{\mathrm{AQCP}}$ + QB1,QB2 + RDP + RSP is sound for AQCP with silent step and guarded linear recursion, modulo quantum rooted branching bisimulation equivalence.

Proof

Since quantum rooted branching bisimulation is both an equivalence and a congruence for AQCP with silent step and guarded linear recursion, only the soundness of the first clause in the definition of the relation = is needed to be checked. That is, if s = t is an axiom in ${\mathcal{E}}_{\mathrm{AQCP}}+$ QB1,QB2 + RDP + RSP and σ a closed substitution that maps the variable in s and t to basic quantum process terms, then we need to check that $\left\langle \sigma (s),\varrho \right\rangle {\underset{\_}{\leftrightarrow}}_{rb}\left\langle \sigma (t),\sigma \right\rangle$.

Since axioms in ${\mathcal{E}}_{\mathrm{AQCP}}$ + QB1,QB2 + RDP + RSP (same as ${\mathcal{E}}_{\mathrm{ACP}}$ + QB1,QB2 + RDP + RSP) are sound for ACP with silent step and guarded linear recursion modulo rooted branching bisimulation equivalence, according to the definition of quantum rooted branching bisimulation, we only need to check if ϱ^′ = σ^′ when ϱ = σ, where ϱ evolves into ϱ^′ after execution of σ(s) and σ evolves into σ^′ after execution of σ(t). We can find that every axiom in Table 5 meets the above condition. □

Theorem 7.4

${\mathcal{E}}_{\mathrm{AQCP}}$ + QB1,QB2 + RDP + RSP is complete for AQCP with silent step and guarded linear recursion, modulo quantum rooted branching bisimulation equivalence.

Proof

To prove that ${\mathcal{E}}_{\mathrm{AQCP}}$ + QB1,QB2 + RDP + RSP is complete for AQCP with silent step and guarded linear recursion modulo quantum rooted branching bisilumation equivalence, it means that $\left\langle s,\varrho \right\rangle {\underset{\_}{\leftrightarrow}}_{rb}\left\langle t,\sigma \right\rangle$ implies s = t.

It was already proved that ${\mathcal{E}}_{\mathrm{AQCP}}$ + QB1,QB2 + RDP + RSP (same as ${\mathcal{E}}_{\mathrm{ACP}}$ + QB1,QB2 + RDP + RSP) is complete for ACP with silent step and guarded linear recursion modulo rooted branching bisimulation equivalence, that is, $s{\underset{\_}{\leftrightarrow}}_{rb}t$ implies s = t. $\left\langle s,\varrho \right\rangle {\underset{\_}{\leftrightarrow}}_{rb}\left\langle t,\sigma \right\rangle$ with ϱ = σ means that $s{\underset{\_}{\leftrightarrow}}_{rb}t$ with ϱ = σ and ϱ^′ = σ^′, where ϱ evolves into ϱ^′ after execution of s and σ evolves into σ^′ after execution of t, according to the definition of quantum rooted branching bisimulation equivalence. The completeness of ${\mathcal{E}}_{\mathrm{AQCP}}$ + QB1,QB2 + RDP + RSP for ACP with silent step and guarded linear recursion modulo rooted branching bisimulation equivalence determines that ${\mathcal{E}}_{\mathrm{AQCP}}$ + QB1,QB2 + RDP + RSP is complete for AQCP with silent step and guarded linear recursion modulo quantum rooted branching bisimulation equivalence. □

7.2 Abstraction

Abstraction operator τ_I is used to abstract away the internal implementations. AQCP extended with silent step τ and abstraction operator τ_I is denoted by AQCP_τ.

7.2.1 Transition Rules of Abstraction Operator

Abstraction operator τ_I(t) renames all labels of transitions of t that are in the set I into τ, and does not change the state of all public quantum variables, which is captured by the following four transition rules.

$$ \frac{\left\langle x,\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle \surd, {\varrho}^{\prime}\right\rangle }{\left\langle {\tau}_I(x),\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle \surd, {\varrho}^{\prime}\right\rangle}\kern1em \upsilon \notin I $$

$$ \frac{\left\langle x,\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle {x}^{\prime },{\varrho}^{\prime}\right\rangle }{\left\langle {\tau}_I(x),\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle {\tau}_I\left({x}^{\prime}\right),{\varrho}^{\prime}\right\rangle}\kern1em \upsilon \notin I $$

$$ \frac{\left\langle x,\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle \surd, {\varrho}^{\prime}\right\rangle }{\left\langle {\tau}_I(x),\varrho \right\rangle \overset{\tau }{\rightarrow}\left\langle \surd, \tau \left(\varrho \right)\right\rangle}\kern1em \upsilon \in I $$

$$ \frac{\left\langle x,\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle {x}^{\prime },{\varrho}^{\prime}\right\rangle }{\left\langle {\tau}_I(x),\varrho \right\rangle \overset{\tau }{\rightarrow}\left\langle {\tau}_I\left({x}^{\prime}\right),\tau \left(\varrho \right)\right\rangle}\kern1em \upsilon \in I $$

Note that ϱ = τ(ϱ) = τ(ϱ^′) in the sense of public variables.

Theorem 7.5

AQCP_τwith guarded linear recursion is a conservative extension of AQCP with silentstep and guarded linear recursion.

Proof

The corresponding TSS of AQCP_τ with guarded linear recursion is a conservative extension of that of AQCP with silent step and guarded linear recursion. That means that AQCP_τ with guarded linear recursion is a conservative extension of AQCP with silent step and guarded linear recursion. □

Theorem 7.6

Quantum rooted branching bisimulation equivalence is a congruence withrespect toAQCP_τwith guarded linear recursion.

Proof

The structural part of QTSSs for AQCP_τ with guarded linear recursion are all in RBB cool format by incorporating the successful termination predicate ↓ in the transition rules, so rooted branching bisimulation equivalence that they induce is a congruence. According to the definition of quantum rooted branching bisimulation, quantum rooted branching bisimulation equivalence that QTSSs for AQCP_τ with guarded linear recursion induce is also a congruence. □

7.2.2 Axiomatization for Abstraction Operator

The axioms for abstraction operator are shown in Table 6.

Table 6 Axioms for abstraction operator

Before we introduce the cluster fair abstraction rule, the concept of cluster is given firstly, which comes from [5].

Definition 7.2 (Cluster)

Let E be a guarded linear recursive specification, and I ⊆ A. Two recursion variable X and Y in E are in the same cluster for I if and only if there exist sequences of transitions $\left\langle X|E\right\rangle \overset{\beta_1}{\rightarrow}\cdots \overset{\beta_m}{\rightarrow}\left\langle Y|E\right\rangle$ and $\left\langle Y|E\right\rangle \overset{\eta_1}{\rightarrow}\cdots \overset{\eta_n}{\rightarrow}\left\langle X|E\right\rangle$, where β₁,⋯ ,β_m, η₁,⋯ ,η_n ∈ I ∪{τ}.

α or αX is an exit for the cluster C if and only if: (1) α or αX is a summand at the right-hand side of the recursive equation for a recursion variable in C, and (2) in the case of αX, either α∉I ∪{τ} or X∉C.

Theorem 7.7

${\mathcal{E}}_{{\mathrm{AQCP}}_{\tau }}$+RSP + RDP + CFAR is sound for AQCP_τwith guarded linear recursion, modulo quantum rooted branching bisimulationequivalence.

Proof

Since quantum rooted branching bisimulation is both an equivalence and a congruence for AQCP_τ with guarded linear recursion, only the soundness of the first clause in the definition of the relation = is needed to be checked. That is, if s = t is an axiom in ${\mathcal{E}}_{{\mathrm{AQCP}}_{\tau }}$ + RSP + RDP + CFAR and σ a closed substitution that maps the variable in s and t to basic quantum process terms, then we need to check that $\left\langle \sigma (s),\varrho \right\rangle {\underset{\_}{\leftrightarrow}}_{rb}\left\langle \sigma (t),\sigma \right\rangle$.

Since axioms in ${\mathcal{E}}_{{\mathrm{AQCP}}_{\tau }}$ + RSP + RDP + CFAR (same as ${\mathcal{E}}_{{\mathrm{ACP}}_{\tau }}$ + RSP + RDP + CFAR) are sound for ACP_τ with guarded linear recursion modulo rooted branching bisimulation equivalence, according to the definition of quantum rooted branching bisimulation, we only need to check if ϱ^′ = σ^′ when ϱ = σ, where ϱ evolves into ϱ^′ after execution of σ(s) and σ evolves into σ^′ after execution of σ(t). We can find that every axiom in Tables 6 and 7 meets the above condition. □

Table 7 Cluster fair abstraction rule

Theorem 7.8

${\mathcal{E}}_{{\mathrm{AQCP}}_{\tau }}$+RSP + RDP + CFAR is complete for AQCP_τwith guarded linear recursion, modulo quantum rooted branching bisimulationequivalence.

Proof

To prove that ${\mathcal{E}}_{{\mathrm{AQCP}}_{\tau }}$ + RSP + RDP + CFAR is complete for AQCP_τ with guarded linear recursion modulo quantum rooted branching bisilumation equivalence, it means that $\left\langle s,\varrho \right\rangle {\underset{\_}{\leftrightarrow}}_{rb}\left\langle t,\sigma \right\rangle$ implies s = t.

It was already proved that ${\mathcal{E}}_{{\mathrm{AQCP}}_{\tau }}$ + RSP + RDP + CFAR (same as ${\mathcal{E}}_{{\mathrm{ACP}}_{\tau }}$ + RSP + RDP + CFAR) is complete for ACP_τ with guarded linear recursion modulo rooted branching bisimulation equivalence, that is, $s{\underset{\_}{\leftrightarrow}}_{rb}t$ implies s = t. $\left\langle s,\varrho \right\rangle {\underset{\_}{\leftrightarrow}}_{rb}\left\langle t,\sigma \right\rangle$ with ϱ = σ means that $s{\underset{\_}{\leftrightarrow}}_{rb}t$ with ϱ = σ and ϱ^′ = σ^′, where ϱ evolves into ϱ^′ after execution of s and σ evolves into σ^′ after execution of t, according to the definition of quantum rooted branching bisimulation equivalence. The completeness of ${\mathcal{E}}_{{\mathrm{AQCP}}_{\tau }}$ + RSP + RDP + CFAR for ACP_τ with guarded linear recursion modulo rooted branching bisimulation equivalence determines that ${\mathcal{E}}_{{\mathrm{AQCP}}_{\tau }}$ + RSP + RDP + CFAR is complete for AQCP_τ with guarded linear recursion modulo quantum rooted branching bisimulation equivalence. □

8 Unifying Quantum and Classical Computing

We use a quantum process configurations 〈p, ϱ〉 to represent information related to the execution of a quantum process, in which p represents the structural properties of a quantum process and ϱ expresses the quantum properties of a quantum process. We have established a whole theory about quantum processes based on ACP, which is called qACP.

In qACP, the set A of actions is consisted of atomic quantum operations, and also the deadlock δ and the silent step τ. The execution of an atomic quantum operation α not only influences of the structural part p, but also changes the state of quantum variables ϱ. We still use the framework of a quantum process configuration p, ϱ under the situation of classical computing. In classical computing, the execution of a (classical) atomic action a only influence the structural part p, and maintain the quantum state ϱ unchanged. Note that, this kind of actions are already introduced in AQCP in Section 5, which are called quantum communicating actions, and range over the set C of quantum communicating actions. In nature, quantum communicating actions are some kind of classical actions in contrast to quantum operations, because they are unrelated to the quantum state ϱ. The difference of a quantum communicating action and a classical communicating action is that they exchange different contents, a classical communicating action exchange the classical data by value or by reference, while a quantum communicating action exchange the quantum variables only by reference. We extend the set C of quantum communicating actions to classical atomic actions (including classical communicating actions), and variables ν, μ range over C, and a, b ∈ C.

Base on the fact that a classical action a does not affect the quantum state ϱ, we can generalize classical ACP under the framework of quantum process configuration 〈p, ϱ〉. We only take an example of BPA, while PAP, ACP, ACP with guarded linear recursion, ACP_τ with guarded linear recursion are omitted.

We give the transition rules under quantum transition system specification (QTSS) for BPA as follows.

$$ \frac{}{\left\langle \upsilon, \varrho \right\rangle \overset{\nu }{\rightarrow}\left\langle \surd, \varrho \right\rangle } $$

$$ \frac{\left\langle x,\varrho \right\rangle \overset{\nu }{\rightarrow}\left\langle \surd, \varrho \right\rangle }{\left\langle x+y,\varrho \right\rangle \overset{\nu }{\rightarrow}\left\langle \surd, \varrho \right\rangle } $$

$$ \frac{\left\langle x,\varrho \right\rangle \overset{\nu }{\rightarrow}\left\langle {x}^{\prime },\varrho \right\rangle }{\left\langle x+y,\varrho \right\rangle \overset{\nu }{\rightarrow}\left\langle {x}^{\prime },\varrho \right\rangle } $$

$$ \frac{\left\langle y,\varrho \right\rangle \overset{\nu }{\rightarrow}\left\langle \surd, \varrho \right\rangle }{\left\langle x+y,\varrho \right\rangle \overset{\nu }{\rightarrow}\left\langle \surd, \varrho \right\rangle } $$

$$ \frac{\left\langle y,\varrho \right\rangle \overset{\nu }{\rightarrow}\left\langle {y}^{\prime },\varrho \right\rangle }{\left\langle x+y,\varrho \right\rangle \overset{\nu }{\rightarrow}\left\langle {y}^{\prime },\varrho \right\rangle } $$

$$ \frac{\left\langle x,\varrho \right\rangle \overset{\nu }{\rightarrow}\left\langle \surd, \varrho \right\rangle }{\left\langle x\cdot y,\varrho \right\rangle \overset{\nu }{\rightarrow}\left\langle y,\varrho \right\rangle } $$

$$ \frac{\left\langle x,\varrho \right\rangle \overset{\nu }{\rightarrow}\left\langle {x}^{\prime },\varrho \right\rangle }{\left\langle x\cdot y,\varrho \right\rangle \overset{\nu }{\rightarrow}\left\langle {x}^{\prime}\cdot y,\varrho \right\rangle } $$

We design an axiomatization ${\mathcal{E}}_{\mathrm{BPA}}$ for BPA modulo quantum bisimulation equivalence as Table 8 shows.

Table 8 Axioms for BPA

We can get the following conclusions naturally.

Theorem 8.1

Quantum bisimulation equivalence is a congruence with respect to BPA.

Theorem 8.2

${\mathcal{E}}_{\mathrm{BPA}}$ is sound for BPA modulo quantum bisimulation equivalence.

Theorem 8.3

${\mathcal{E}}_{\mathrm{BPA}}$ is complete for BPA modulo quantum bisimulation equivalence.

Note that, the behavior of deadlock constant δ quantum computing is the same as that of classical computing. But, the behavior of silent step τ is different under the framework of quantum process configuration 〈p, ϱ〉 for quantum computing and classical computing, just because τ in quantum computing can affect the state of all quantum variables, while τ in classical computing really keeps silent.

Making classical ACP (including BPA, PAP, ACP, ACP with guarded linear recursion, and ACP_τ with guarded linear recursion) being under the framework of quantum process configuration 〈p, ϱ〉 for classical computing is trivial, because ϱ is meaningless only for classical computing. But, in the view of unifying quantum computing and classical computing, this work would be very important. Fortunately, qACP and classical ACP are unified under the framework of quantum process configuration 〈p, ϱ〉, that is, qACP and classical ACP have the same equational logic (axiomatization ${\mathcal{E}}_{\mathrm{qACP}}$ and ${\mathcal{E}}_{\mathrm{ACP}}$) and the same semantic model (strong quantum bisimilarity and weak quantum bisimilarity).

The unifying of qACP and classical ACP has an important significance, because most quantum protocols, like the famous BB84 protocol [18], are mixtures of quantum information and classical information, and those of quantum computing and classical computing. This unifying can be used widely in verification for all quantum protocols.

9 Verification for Quantum Protocols – the BB84 Protocol

The unifying of qACP and classical ACP under the framework of quantum process configuration 〈p, ϱ〉 makes verification for quantum protocols possible, not only the pure quantum protocol, but also protocol that mixes quantum information and classical information.

The famous BB84 protocol [18] is the first quantum key distribution protocol, in which quantum information and classical information are mixed. We take an example of the BB84 protocol to illustrate the usage of qACP in verification of quantum protocols.

The BB84 protocol is used to create a private key between two parities, Alice and Bob. Firstly, we introduce the basic BB84 protocol briefly, which is illustrated in Fig. 1.

• 1. Alice create two string of bits with size n randomly, denoted as B_a and K_a.

• 2. Alice generates a string of qubits q with size n, and the i th qubit in q is |x_y〉, where x is the i th bit of B_a and y is the i th bit of K_a.

• 3. Alice sends q to Bob through a quantum channel Q between Alice and Bob.

• 4. Bob receives q and randomly generates a string of bits B_b with size n.

• 5. Bob measures each qubit of q according to a basis by bits of B_b. And the measurement results would be K_b, which is also with size n.

• 6. Bob sends his measurement bases B_b to Alice through a public channel P.

• 7. Once receiving B_b, Alice sends her bases B_a to Bob through channel P, and Bob receives B_a.

• 8. Alice and Bob determine that at which position the bit strings B_a and B_b are equal, and they discard the mismatched bits of B_a and B_b. Then the remaining bits of K_a and K_b, denoted as ${K}_a^{\prime }$ and ${K}_b^{\prime }$ with ${K}_{a,b}={K}_a^{\prime }={K}_b^{\prime }$.

Fig. 1

The BB84 protocol

We re-introduce the basic BB84 protocol in an abstract way with more technical details as Fig. 1 illustrates.

Now, we assume a special measurement operation Rand[q;B_a] which create a string of n random bits B_a from the q quantum system, and the same as Rand[q;K_a], Rand[q^′;B_b]. M[q;K_b] denotes the Bob’s measurement operation of q. The generation of n qubits q through two quantum operations $Se{t}_{K_a}\left[q\right]$ and ${H}_{B_a}\left[q\right]$. Alice sends q to Bob through the quantum channel Q by quantum communicating action send_Q(q) and Bob receives q through Q by quantum communicating action receive_Q(q). Bob sends B_b to Alice through the public channel P by classical communicating action send_P(B_b) and Alice receives B_b through channel P by classical communicating action receive_P(B_b), and the same as send_P(B_a) and receive_P(B_a). Alice and Bob generate the private key K_{a, b} by a classical comparison action cmp(K_{a, b}, K_a, K_b, B_a, B_b). Let Alice and Bob be a system AB and let interactions between Alice and Bob be internal actions. AB receives external input D_i through channel A by communicating action receive_A(D_i) and sends results D_o through channel B by communicating action send_B(D_o).

Then the state transition of Alice can be described by qACP as follows.

$$ {\displaystyle \begin{array}{rcl}A& =& \sum \limits_{D_i\in {\varDelta}_i} receiv{e}_A\left({D}_i\right)\cdot {A}_1\\ {}{A}_1& =& Rand\left[q;{B}_a\right]\cdot {A}_2\\ {}{A}_2& =& Rand\left[q;{K}_a\right]\cdot {A}_3\\ {}{A}_3& =& Se{t}_{K_a}\left[q\right]\cdot {A}_4\\ {}{A}_4& =& {H}_{B_a}\left[q\right]\cdot {A}_5\\ {}{A}_5& =& sen{d}_Q(q)\cdot {A}_6\\ {}{A}_6& =& receiv{e}_P\left({B}_b\right)\cdot {A}_7\\ {}{A}_7& =& sen{d}_P\left({B}_a\right)\cdot {A}_8\\ {}{A}_8& =& cmp\left({K}_{a,b},{K}_a,{K}_b,{B}_a,{B}_b\right)\cdot A\end{array}} $$

where Δ_i is the collection of the input data.

And the state transition of Bob can be described by qACP as follows.

$$ {\displaystyle \begin{array}{rcl}B& =& receiv{e}_Q(q)\cdot {B}_1\\ {}{B}_1& =& Rand\left[{q}^{\prime };{B}_b\right]\cdot {B}_2\\ {}{B}_2& =& M\left[q;{K}_b\right]\cdot {B}_3\\ {}{B}_3& =& sen{d}_P\left({B}_b\right)\cdot {B}_4\\ {}{B}_4& =& receiv{e}_P\left({B}_a\right)\cdot {B}_5\\ {}{B}_5& =& cmp\left({K}_{a,b},{K}_a,{K}_b,{B}_a,{B}_b\right)\cdot {B}_6\\ {}{B}_6& =& \sum \limits_{D_o\in {\varDelta}_o} sen{d}_B\left({D}_o\right)\cdot B\end{array}} $$

where Δ_o is the collection of the output data.

The send action and receive action of the same data through the same channel can communicate each other, otherwise, a deadlock δ will be caused. We define the following communication functions.

$$ {\displaystyle \begin{array}{rcl}& & \gamma \left( sen{d}_Q(q), receiv{e}_Q(q)\right)\triangleq {c}_Q(q)\\ {}& & \gamma \left( sen{d}_P\left({B}_b\right), receiv{e}_P\left({B}_b\right)\right)\triangleq {c}_P\left({B}_b\right)\\ {}& & \gamma \left( sen{d}_P\left({B}_a\right), receiv{e}_P\left({B}_a\right)\right)\triangleq {c}_P\left({B}_a\right)\end{array}} $$

Let A and B in parallel, then the system AB can be represented by the following process term.

$$ {\tau}_I\left({\partial}_H\left(A\parallel B\right)\right) $$

where H = {send_Q(q), receive_Q(q), send_P(B_b), receive_P(B_b), send_P(B_a), receive_P(B_a)} and $I=\Big\{ Rand\left[q;{B}_a\right], Rand\left[q;{K}_a\right], Se{t}_{K_a}\left[q\right],{H}_{B_a}\left[q\right], Rand\left[{q}^{\prime };{B}_b\right],M\left[q;{K}_b\right]$, c_Q(q),c_P(B_b), c_P(B_a), cmp(K_{a, b}, K_a, K_b, B_a, B_b)}.

Then we get the following conclusion.

Theorem 9.1

The basic BB84 protocol τ_I(∂_H(A ∥ B)) exhibits desired external behaviors.

Proof

$$ {\displaystyle \begin{array}{rcl}& & {\partial}_H\left(A\parallel B\right)=\sum \limits_{D_i\in {\varDelta}_i} receiv{e}_A\left({D}_i\right)\cdot {\partial}_H\left({A}_1\parallel B\right)\\ {}& & {\partial}_H\left({A}_1\parallel B\right)= Rand\left[q;{B}_a\right]\cdot {\partial}_H\left({A}_2\parallel B\right)\\ {}& & {\partial}_H\left({A}_2\parallel B\right)= Rand\left[q;{K}_a\right]\cdot {\partial}_H\left({A}_3\parallel B\right)\\ {}& & {\partial}_H\left({A}_3\parallel B\right)= Se{t}_{K_a}\left[q\right]\cdot {\partial}_H\left({A}_4\parallel B\right)\\ {}& & {\partial}_H\left({A}_4\parallel B\right)={H}_{B_a}\left[q\right]\cdot {\partial}_H\left({A}_5\parallel B\right)\\ {}& & {\partial}_H\left({A}_5\parallel B\right)={c}_Q(q)\cdot {\partial}_H\left({A}_6\parallel {B}_1\right)\\ {}& & {\partial}_H\left({A}_6\parallel {B}_1\right)= Rand\left[{q}^{\prime };{B}_b\right]\cdot {\partial}_H\left({A}_6\parallel {B}_2\right)\\ {}& & {\partial}_H\left({A}_6\parallel {B}_2\right)=M\left[q;{K}_b\right]\cdot {\partial}_H\left({A}_6\parallel {B}_3\right)\\ {}& & {\partial}_H\left({A}_6\parallel {B}_3\right)={c}_P\left({B}_b\right)\cdot {\partial}_H\left({A}_7\parallel {B}_4\right)\\ {}& & {\partial}_H\left({A}_7\parallel {B}_4\right)={c}_P\left({B}_a\right)\cdot {\partial}_H\left({A}_8\parallel {B}_5\right)\\ {}& & {\partial}_H\left({A}_8\parallel {B}_5\right)= cmp\left({K}_{a,b},{K}_a,{K}_b,{B}_a,{B}_b\right)\cdot {\partial}_H\left(A\parallel {B}_5\right)\\ {}& & {\partial}_H\left(A\parallel {B}_5\right)= cmp\left({K}_{a,b},{K}_a,{K}_b,{B}_a,{B}_b\right)\cdot {\partial}_H\left(A\parallel {B}_6\right)\\ {}& & {\partial}_H\left(A\parallel {B}_6\right)=\sum \limits_{D_o\in {\varDelta}_o} sen{d}_B\left({D}_o\right)\cdot {\partial}_H\left(A\parallel B\right)\end{array}} $$

Let ∂_H(A ∥ B) = 〈X₁|E〉, where E is the following guarded linear recursion specification:

$$ {\displaystyle \begin{array}{rcl}\Big\{{X}_1& =& \sum \limits_{D_i\in {\varDelta}_i} receiv{e}_A\left({D}_i\right)\cdot {X}_2,{X}_2= Rand\left[q;{B}_a\right]\cdot {X}_3,{X}_3= Rand\left[q;{K}_a\right]\cdot {X}_4,\\ {}{X}_4& =& Se{t}_{K_a}\left[q\right]\cdot {X}_5,{X}_5={H}_{B_a}\left[q\right]\cdot {X}_6,{X}_6={c}_Q(q)\cdot {X}_7,\\ {}{X}_7& =& Rand\left[{q}^{\prime };{B}_b\right]\cdot {X}_8,{X}_8=M\left[q;{K}_b\right]\kern-.1em \cdot \kern-.1em {X}_9,{X}_9={c}_P\left({B}_b\right)\cdot {X}_{10},{X}_{10}={c}_P\left({B}_a\right)\cdot {X}_{11},\\ {}{X}_{11}& =& cmp\left({K}_{a,b},{K}_a,{K}_b,{B}_a,{B}_b\right)\cdot {X}_{12},{X}_{12}= cmp\left({K}_{a,b},{K}_a,{K}_b,{B}_a,{B}_b\right)\cdot {X}_{13},\\ {}{X}_{13}& =& \sum \limits_{D_o\in {\varDelta}_o} sen{d}_B\left({D}_o\right)\cdot {X}_1\Big\}\end{array}} $$

Then we apply abstraction operator τ_I into 〈X₁|E〉.

$$ {\displaystyle \begin{array}{rcl}{\tau}_I\left(\left\langle {X}_1|E\right\rangle \right)& =& \sum \limits_{D_i\in {\varDelta}_i} receiv{e}_A\left({D}_i\right)\cdot {\tau}_I\left(\left\langle {X}_2|E\right\rangle \right)\\ {}& =& \sum \limits_{D_i\in {\varDelta}_i} receiv{e}_A\left({D}_i\right)\cdot {\tau}_I\left(\left\langle {X}_3|E\right\rangle \right)\\ {}& =& \sum \limits_{D_i\in {\varDelta}_i} receiv{e}_A\left({D}_i\right)\cdot {\tau}_I\left(\left\langle {X}_4|E\right\rangle \right)\\ {}& =& \sum \limits_{D_i\in {\varDelta}_i} receiv{e}_A\left({D}_i\right)\cdot {\tau}_I\left(\left\langle {X}_5|E\right\rangle \right)\\ {}& =& \sum \limits_{D_i\in {\varDelta}_i} receiv{e}_A\left({D}_i\right)\cdot {\tau}_I\left(\left\langle {X}_6|E\right\rangle \right)\\ {}& =& \sum \limits_{D_i\in {\varDelta}_i} receiv{e}_A\left({D}_i\right)\cdot {\tau}_I\left(\left\langle {X}_7|E\right\rangle \right)\\ {}& =& \sum \limits_{D_i\in {\varDelta}_i} receiv{e}_A\left({D}_i\right)\cdot {\tau}_I\left(\left\langle {X}_8|E\right\rangle \right)\\ {}& =& \sum \limits_{D_i\in {\varDelta}_i} receiv{e}_A\left({D}_i\right)\cdot {\tau}_I\left(\left\langle {X}_9|E\right\rangle \right)\\ {}& =& \sum \limits_{D_i\in {\varDelta}_i} receiv{e}_A\left({D}_i\right)\cdot {\tau}_I\left(\left\langle {X}_{10}|E\right\rangle \right)\\ {}& =& \sum \limits_{D_i\in {\varDelta}_i} receiv{e}_A\left({D}_i\right)\cdot {\tau}_I\left(\left\langle {X}_{11}|E\right\rangle \right)\\ {}& =& \sum \limits_{D_i\in {\varDelta}_i} receiv{e}_A\left({D}_i\right)\cdot {\tau}_I\left(\left\langle {X}_{12}|E\right\rangle \right)\\ {}& =& \sum \limits_{D_i\in {\varDelta}_i} receiv{e}_A\left({D}_i\right)\cdot {\tau}_I\left(\left\langle {X}_{13}|E\right\rangle \right)\\ {}& =& \sum \limits_{D_i\in {\varDelta}_i}\sum \limits_{D_o\in {\varDelta}_o} receiv{e}_A\left({D}_i\right)\cdot sen{d}_B\left({D}_o\right)\cdot {\tau}_I\left(\left\langle {X}_1|E\right\rangle \right)\end{array}} $$

We get ${\tau}_I\left(\left\langle {X}_1|E\right\rangle \right)={\sum}_{D_i\in {\varDelta}_i}{\sum}_{D_o\in {\varDelta}_o} receiv{e}_A\left({D}_i\right)\cdot sen{d}_B\left({D}_o\right)\cdot {\tau}_I\left(\left\langle {X}_1|E\right\rangle \right)$, that is, ${\tau}_I\left({\partial}_H\left(A\parallel B\right)\right)={\sum}_{D_i\in {\varDelta}_i}{\sum}_{D_o\in {\varDelta}_o} receiv{e}_A\left({D}_i\right)\cdot sen{d}_B\left({D}_o\right)\cdot {\tau}_I\left({\partial}_H\left(A\parallel B\right)\right)$. So, the basic BB84 protocol τ_I(∂_H(A ∥ B)) exhibits desired external behaviors. □

10 Extensions – Renaming Operator

One of the most fascinating characteristics is the modularity of ACP, that is, ACP can be extended easily. Through out this paper, we can see that qACP also inherents the modularity characteristics of ACP. By introducing new operators or new constants, qACP can have more properties. It is already proved that ACP or qACP possibly has the same expressive power as a Turing machine [7]. Though extensions can not improve the expressive power of qACP, but they provide qACP an elegant fashion to express a new property.

In this section, we take an example of renaming operator which is used to rename the atomic quantum operations.

10.1 Transition Rules of Renaming Operators

Renaming operator ϱ_f(t) renames all actions in process term t, and the change of the quantum state is consistent, which is expressed by the following two transition rules.

$$ \frac{\left\langle x,\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle \surd, {\varrho}^{\prime}\right\rangle }{\left\langle {\varrho}_f(x),\varrho \right\rangle \overset{f\left(\upsilon \right)}{\rightarrow}\left\langle \surd, {\varrho}^{\prime}\right\rangle } $$

$$ \frac{\left\langle x,\varrho \right\rangle \overset{\upsilon }{\rightarrow}\left\langle {x}^{\prime },{\varrho}^{\prime}\right\rangle }{\left\langle {\varrho}_f(x),\varrho \right\rangle \overset{f\left(\upsilon \right)}{\rightarrow}\left\langle {\varrho}_f\left({x}^{\prime}\right),{\varrho}^{\prime}\right\rangle } $$

Theorem 10.1

AQCP_τwithguarded linear recursion and renaming operators is a conservative extension of AQCP_τwith guarded linear recursion.

Proof

The corresponding TSS of AQCP_τ with guarded linear recursion and renaming operators is a conservative extension of that of AQCP_τ with guarded linear recursion. That means that AQCP_τ with guarded linear recursion and renaming operators is a conservative extension of AQCP_τ with guarded linear recursion. □

Theorem 10.2

Quantum rooted branching bisimulation equivalence is a congruence withrespect toAQCP_τwith guarded linear recursion and renaming operators.

Proof

The structural part of QTSSs for AQCP_τ with guarded linear recursion and renaming operators are all in RBB cool format by incorporating the successful termination predicate ↓ in the transition rules, so rooted branching bisimulation equivalence that they induce is a congruence. According to the definition of quantum rooted branching bisimulation, quantum rooted branching bisimulation equivalence that QTSSs for AQCP_τ with guarded linear recursion and renaming operators induce is also a congruence. □

10.2 Axioms for Renaming Operators

The axioms for renaming operator is shown in Table 9.

Table 9 Axioms for renaming

Theorem 10.3

${\mathcal{E}}_{{\mathrm{AQCP}}_{\tau }}$+RSP + RDP + CFAR + QRN1-QRN4 is sound forAQCP_τwith guarded linear recursion and renaming operators, modulo quantum rootedbranching bisimulation equivalence.

Proof

Since quantum rooted branching bisimulation is both an equivalence and a congruence for AQCP_τ with guarded linear recursion and renaming operators, only the soundness of the first clause in the definition of the relation = is needed to be checked. That is, if s = t is an axiom in ${\mathcal{E}}_{{\mathrm{AQCP}}_{\tau }}$ + RSP + RDP + CFAR + QRN1-QRN4 and σ a closed substitution that maps the variable in s and t to basic quantum process terms, then we need to check that $\left\langle \sigma (s),\varrho \right\rangle {\underset{\_}{\leftrightarrow}}_{rb}\left\langle \sigma (t),\sigma \right\rangle$.

Since axioms in ${\mathcal{E}}_{{\mathrm{AQCP}}_{\tau }}$ + RSP + RDP + CFAR + QRN1-QRN4 (same as ${\mathcal{E}}_{{\mathrm{ACP}}_{\tau }}$ + RSP + RDP + CFAR + QRN1-QRN4) are sound for ACP_τ with guarded linear recursion and renaming operators modulo rooted branching bisimulation equivalence, according to the definition of quantum rooted branching bisimulation, we only need to check if ϱ^′ = σ^′ when ϱ = σ, where ϱ evolves into ϱ^′ after execution of σ(s) and σ evolves into σ^′ after execution of σ(t). We can find that every axiom in Table 9 meets the above condition. □

Theorem 10.4

${\mathcal{E}}_{{\mathrm{AQCP}}_{\tau }}$+RSP + RDP + CFAR + QRN1-QRN4 is complete forAQCP_τwith guarded linear recursion and renaming operators, modulo quantum rootedbranching bisimulation equivalence.

Proof

To prove that ${\mathcal{E}}_{{\mathrm{AQCP}}_{\tau }}$ + RSP + RDP + CFAR + QRN1-QRN4 is complete for AQCP_τ with guarded linear recursion and renaming operators modulo quantum rooted branching bisilumation equivalence, it means that $\left\langle s,\varrho \right\rangle {\underset{\_}{\leftrightarrow}}_{rb}\left\langle t,\sigma \right\rangle$ implies s = t.

It was already proved that ${\mathcal{E}}_{{\mathrm{AQCP}}_{\tau }}$ + RSP + RDP + CFAR + QRN1-QRN4 (same as ${\mathcal{E}}_{{\mathrm{ACP}}_{\tau }}$ + RSP + RDP + CFAR + QRN1-QRN4) is complete for ACP_τ with guarded linear recursion and renaming operators modulo rooted branching bisimulation equivalence, that is, $s{\underset{\_}{\leftrightarrow}}_{rb}t$ implies s = t. $\left\langle s,\varrho \right\rangle {\underset{\_}{\leftrightarrow}}_{rb}\left\langle t,\sigma \right\rangle$ with ϱ = σ means that $s{\underset{\_}{\leftrightarrow}}_{rb}t$ with ϱ = σ and ϱ^′ = σ^′, where ϱ evolves into ϱ^′ after execution of s and σ evolves into σ^′ after execution of t, according to the definition of quantum rooted branching bisimulation equivalence. The completeness of ${\mathcal{E}}_{{\mathrm{AQCP}}_{\tau }}$ + RSP + RDP + CFAR + QRN1-QRN4 for ACP_τ with guarded linear recursion and renaming operators modulo rooted branching bisimulation equivalence determines that ${\mathcal{E}}_{{\mathrm{AQCP}}_{\tau }}$ + RSP + RDP + CFAR + QRN1-QRN4 is complete for AQCP_τ with guarded linear recursion and renaming operators modulo quantum rooted branching bisimulation equivalence. □

We can see that qACP with renaming operator and ACP with renaming operator can also be unified under the framework of quantum process configuration 〈p, ϱ〉.

11 Conclusions

In this paper, we extend the traditional structural operational semantics under the framework of quantum process configuration 〈p, ϱ〉 to support quantum processes. Based on the relationship between quantum bisimilarity and classical bisimilarity, we establish a series of axiomatization for quantum processes called qACP. We also unify qACP and classical ACP under the framework of quantum process configuration 〈p, ϱ〉. It makes qACP can adapt to all quantum communication protocols.

Now, we point out some future directions. (1) Quantum entanglement makes the processing of the silent step τ somewhat strange. The nature of influence of quantum entanglement for computation, especially for parallelism and concurrency, should be considered carefully and deeply in future, because quantum entanglement is unique for quantum mechanics. (2) Other novel framework representing quantum processes should be proposed, not only the quantum process configuration 〈p, ϱ〉. New framework will unify quantum computing and classical computing in a new way, which maybe capture the nature of quantum computing more naturally. (3) qACP inherits the modularity of ACP and makes it can be extended in an elegant fashion, in future, more properties can be extended in qACP. (4) The axiomatization of qACP can be used to verify most quantum communication protocols easily and widely in future.