arXiv:quant-ph/0508116v1 16 Aug 2005

A Probabilistic Branching Bisimulation for
Quantum Processes
Marie L ALIRE∗
Leibniz Laboratory
46, avenue Félix Viallet - 38000 Grenoble, France
12th August 2017

Abstract
Full formal descriptions of algorithms making use of quantum principles
must take into account both quantum and classical computing components
and assemble them so that they communicate and cooperate. Moreover, to
model concurrent and distributed quantum computations, as well as quantum communication protocols, quantum to quantum communications which
move qubits physically from one place to another must also be taken into
account.
Inspired by classical process algebras, which provide a framework for
modeling cooperating computations, a process algebraic notation is defined,
which provides a homogeneous style to formal descriptions of concurrent
and distributed computations comprising both quantum and classical parts.
Based upon an operational semantics which makes sure that quantum objects, operations and communications operate according to the postulates of
quantum mechanics, a probabilistic branching bisimulation is defined among
processes considered as having the same behavior.

1

Introduction

Quantum algorithms are frequently described by means of quantum gate networks.
This has several drawbacks, for instance, gate networks do not allow descriptions
of loops nor conditional executions of parts of networks. So as to overcome these
∗ Marie.Lalire@imag.fr

1

difficulties, a few quantum programming languages have been developed, such
as: QCL [12], an imperative language designed by Bernhard Ömer which aims at
simulating quantum programs, qGCL [15] by Paolo Zuliani which allows the construction of proved correct quantum programs through a refinement method, QPL
[13], a functional language designed by Peter Selinger with a denotational semantics, and a few others. Several quantum λ-calculus have also been developed:
for example [14] by André Van Tonder, which is based on a simplified linear λcalculus and [2] by Pablo Arrighi and Gilles Dowek, which is a ”linear-algebraic
λ-calculus”.
Cooperation between quantum and classical computations is inherent in quantum algorithmics. Teleportation of a qubit state from Alice to Bob [4] is a good
example of this cooperation. Indeed, Alice carries out a measurement, the result
of which (two bits) is sent to Bob, and Bob uses this classical result to determine which quantum transformation he must apply. Moreover, initial preparation
of quantum states and measurement of quantum results are two essential forms
of interactions between the classical and quantum parts of computations which a
language must be able to express. Process algebras are a good candidate for such
a language since they provide a framework for modeling cooperating computations. In addition, they have well defined semantics and permit the transformation
of programs as well as the formal study and analysis of their properties. A key
point in their semantics is the definition of an equivalence relation on processes.
Bisimulation is an adequate equivalence relation to deal with communicating processes since it relates processes that can execute the same flows of actions while
having the same branching structure.
Simon Gay and Rajagopal Nagarajan have also developed CQP, a language
to describe communicating quantum processes [11]. This language is based on
π-calculus. An important point in their work is the definition of a type system,
and the proof that the operational semantics preserves typing.
This paper presents first the main points of the definition of a Quantum Process
Algebra (QPAlg). Then, examples of short quantum programs are given in section
3. Finally, a bisimulation among processes is defined in section 4.

2

Quantum communicating processes

The process algebra developed here is based upon process algebras such as CCS
[10] and Lotos [5]. In this process algebra, basic actions are communications
among processes (emission, denoted g !x and reception, denoted g ?x , where g
is a communication gate) and quantum actions (unitary transformations and mea-

2

surements). To create a process from basic actions, the prefix operator ”.” is used:
if α is an action and P , a process, α.P is a new process which performs α first,
then behaves as P .
There are two predefined processes: nil, the process that cannot perform any
transition, and end, which performs a ”δ-transition” for signaling successful termination, and becomes nil (”δ-transitions” are necessary in the semantics of sequential composition of processes).
The operators of the process algebra are: sequential composition (P ; Q), parallel composition (P k Q), conditional choice ([[ c1 → P1 , . . . , cn → Pn ] ) and
restriction (P \L ). As for sequential composition, process Q is executed if process
P terminates successfully, that is to say if P performs a δ-transition. The process
[ c1 → P1 , . . . , cn → Pn ] , where ci is a condition and Pi a process, evolves as a
process chosen nondeterministically among the processes Pj such that cj is true.
Restriction is useful for disallowing the use of some gates (the gates listed in L),
thus forcing internal communication within process P . Communication can occur
between two parallel processes whenever a value emission in one of them and a
value reception in the other one use the same gate name.
The main points of QPAlg involving the quantum world are developed in the
rest of this section. The precise syntax and the main inference rules of the semantics are given in appendix A. For more details, see [9].

2.1

Quantum variables

For the purpose of this paper, we consider that there are two types of variables,
one classical: Nat, for variables taking integer values, and one quantum: Qubit for
variables standing for qubits. An extended version of the process algebra would
of course also include quantum registers and other types of variables.
In classical process algebras, variables are instantiated when communications
between processes occur and cannot be modified after their instantiation. As a
consequence, it is not necessary to store their values. In fact, when a variable is
instantiated, all its occurrences are replaced by the value received.
Here, quantum variables stand for physical qubits. Applying a unitary transformation to a variable which represents a qubit modifies the state of that qubit.
This means that values of variables are modified. For that reason, it is necessary
to keep track of both variable names and variable states.
Variables are declared, the syntax is: [ x1 : t1 , . . . , xn : tn . P ] where
x1 , . . . , xn is a list of variables, t1 , . . . , tn are their types, and P is a process
which can make use of these classical and quantum variables. To simplify the rest
of this paper, the names of variables will always be considered distinct.

3

In the inference rules which describe the semantics of processes, the states of
processes are process terms P together with contexts C, of the form P/C. The
main purpose of a context is to maintain the quantum state, stored as q = ρ where
q is a sequence of quantum variable names and ρ a density matrix representing
their current quantum state. Moreover, in order to treat classical variables in a
similar way, modifications of classical variables are also allowed. So, for the
same reason as in the case of quantum variables, classical values are stored in
the context. Storing and retrieving classical values is represented by functions
f : names → values. The context must also keep track of the embedding of
variable scopes. To keep track of parallel composition, this is done via a ”cactus
stack” structure of sets of variables, called the environment stack (s), which stores
variable scopes and types. The set of all the variables in s is denoted Var(s), ”.”
adds an element on top of a stack, and ”|” concatenates two stacks.
In summary, the context has three components < s, q = ρ, f >, where:
• s is the environment stack;
• q is a sequence of quantum variable names;
• ρ is a density matrix representing the quantum state of the variables in q;
• f is the function which associates values with classical variables.
The rules for declaration and liberation of variables are the following:
Declaration:
[ x1 : t1 , . . . , xn : tn . P ] /C

′
−−τ−→ [ P ] /C

with C =< s, q = ρ, f >, C ′ =< s′ , q = ρ, f >
and s′ = {(x1 , t1 ), . . . , (xn , tn )}.s
This rule adds the new variable names and types on top of the stack s. Because
the variables do not have values yet, the quantum state and the classical function
do not have to be modified at this point.
Evolution of a process within the scope of declared variables:
P/C
[ P ] /C

′
′
−−α
−→ P /C
′
′
−−α
−→ [ P ] /C

4

α 6= δ

In short: if the process P can perform a transition, then the process [ P ] can
perform the same transition, provided that the action of the transition is not δ.
Termination of a process with exit from a scope and liberation of the variables:
′
−−δ−→ P / < e.s, q = ρ, f >
nil / < s, q\Var(e) = T rVar(e)/q (ρ), f \Var(e) >

P/C
[ P ] /C

δ
−−−→

If the action is δ, this means that P has successfully terminated, so the context
must be cleaned up by eliminating the variables having their scope limited to that
process. These variables have their names listed in the head e of the stack. So,
cleaning up the context means eliminating the head of the stack, removing the
variables in e from the sequence q and from the domain of the function f . The
new quantum state is obtained by performing a partial trace on ρ over the qubits
in Var(e), which is denoted T rVar(e)/q (ρ).

2.2

Basic actions

The classical basic actions are classical to classical communications and will not
be further defined here. Classical to quantum communications and quantum to
quantum communications are introduced for respectively initializing qubits and
allowing the description of quantum communication protocols. Quantum to classical communications are part of measurement and are dealt with in the next paragraph.
The semantics of communications involving the quantum world is based upon
the following rules concerning the quantum side of such communications:
g !x .P/C

g !x
−−−−−−→

P/C ′

where
• C =< s, q = ρ, f > and C ′ =< s\{x}, q\{x} = T r{x}/q (ρ), f >
• x ∈ Var(s) and x ∈ q
and:
g ?x .P/C

g ?x
P/C ′
−−−−−−→

where
5

• C =< s, q = ρ, f >, C ′ =< s, x.q = ν ⊗ ρ, f >
• x ∈ Var(s), x of type Qubit, x 6∈ q
• ν density matrix of dimension 2
The first rule deals with qubit sending, and the other one, with reception of a
qubit. For qubit sending, because of the no-cloning theorem, the sent qubit must
be removed from the context. The two rules concerning classical value sending
and classical value reception are given in appendix A.2.
In the operational semantics of parallel composition, the combination of the
rules for emission and reception defines communication. In a classical to quantum communication, the qubit is initialized in the basis state |vihv|, where v is
the classical value sent (in this case, v must be 0 or 1). In a quantum to quantum
communication, the name of the sent qubit is replaced in q by the name of the
receiving qubit.
Other basic actions are unitary transformations which perform the unitary evolution of qubit states. Given a set U of predefined unitary transformations, the
action corresponding to the application of U ∈ U to a list of quantum variables is
denoted by U [x1 , . . . , xn ].
The inference rule for unitary transformations is:
U [x1 , . . . , xn ].P/ < s, q = ρ, f >

′
−−τ−→ P/ < s, q = ρ , f >

where
• U ∈ U, x1 , . . . , xn ∈ Var(s), and x1 , . . . , xn ∈ q
• x1 , . . . , xn are pairwise distinct
• ρ′ = TU (ρ)
The condition x1 , . . . , xn ∈ q prevents from applying a unitary transformation
to qubits which have not been initialized.
TU is the super-operator which must be applied to ρ, to describe the evolution
of the quantum state due to the application of the unitary transformation U to the
qubits x1 , . . . , xn . In general, with A a 2n × 2n matrix:
TA : ρ 7→ Π† .(A ⊗ I ⊗k ).Π.ρ.Π† .(A† ⊗ I ⊗k ).Π
where
6

• Π is the permutation matrix which places the xi ’s at the head of q
• k = size(q) − n
• I ⊗k = I ⊗ · · · ⊗ I , where I is the identity matrix on C2
| {z }
k

Since the unitary transformation U may be applied to qubits which are anywhere within the list q, a permutation Π must be applied first. This permutation
moves the xi ’s so that they are placed at the head of q in the order specified by
[x1 , . . . , xn ]. Then U can be applied to the first n elements and I to the remainder.
Finally, the last operation is the inverse of the permutation Π so that at the end,
the arrangement of the elements in ρ is consistent with the order of the elements
in q.

2.3

Measurement and probabilistic processes

Last but not least, an essential basic action has to be introduced into the process
algebra: quantum measurement. Let M be an observable in a set O of predefined
observables, x1 , . . . , xn a list of distinct quantum variables and g a gate. The
syntax for measurement is the following:
• M [x1 , . . . , xn ] is a measurement of the n qubits of the list with respect to
observable M , but the classical result is neither stored nor transmitted.
• g !M [x1 , . . . , xn ] is a measurement of the n qubits of the list with respect
to observable M , followed by sending the classical result through gate g.
Measurement is probabilistic: more precisely, the classical result and the quantum state after measurement are probabilistic. In the case of measurement without
communication of the classical result, only the quantum state is probabilistic after
measurement, so the probabilities can be reflected in the density matrix:
M [x1 , . . . , xn ].P/ < s, q = ρ, f >

′
−−τ−→ P/ < s, q = ρ , f >

with
• x1 , . . . , xn ∈ Var(s), x1 , . . . , xn ∈ q and x1 , . . . , xn are pairwise distinct
P
• M ∈ O with i λi Pi as spectral decomposition
P
• ρ′ = i TPi (ρ)
7

As in the case of unitary transformations, TPi is the super-operator corresponding
to the application of the projector Pi to measured qubits. The computation of ρ′
stems from the projective measurement postulate of quantum mechanics.
When the value coming out of the measurement is sent out, the classical result
is probabilistic. This requires the introduction of a probabilistic composition operator for contexts. This operator is denoted ⊞p : the state P/C1 ⊞p C2 is P/C1
with probability p and P/C2 with probability 1 − p. In general, a context is either
of the form < s, q = ρ, f >, or of the form ⊞pi < si , qi = ρi , fi > where the pi ’s
are probabilities adding to 1. Then, the rule for measurement followed by sending
the classical result is:
g !M [x1 , . . . , xn ] .P/C

τ
[ g !y .end ] ; P/ ⊞pi Ci
−−−→

where
• C =< s, q = ρ, f >
• Ci =< {(y, Nat)}.s, q = ρi , f ∪ {y 7→ λi } >
• x1 , . . . , xn ∈ Var(s), x1 , . . . , xn ∈ q and x1 , . . . , xn are pairwise distinct
• y is a new variable (introduced as y : Nat by this rule)
P
• M ∈ O with i λi Pi as spectral decomposition
• pi = T r(TPi (ρ)),

ρi =

1
pi TPi (ρ)

As explained in [6] and [7], if a process contains both a probabilistic and a
nondeterministic choice, the probabilistic choice must always be solved first. In
the process algebra presented here, nondeterminism appears with parallel composition and conditional choice. So as to guarantee that probabilistic choice is
always solved first, the notion of probabilistic stability for contexts is introduced:
a context C is probabilistically stable, which is denoted C ↓, if it is of the form
< s, q = ρ, f >. If the context of a process state is not stable, a probabilistic
transition must be performed first:
X
pi = 1
where
P/ ⊞pi Ci −→pj P/Cj
i
where S1 −→p S2 means that state S1 becomes S2 with probability p.

8

3

Examples

In the following examples, the set U of unitary transformations is:
U = {H, CN ot, I, X, Y, Z}
where H is Hadamard transformation, CN ot is ”controlled not”, I is the identity,
and X, Y, Z are Pauli operators. The set O of observables contains the observables corresponding to measurement of one and two qubits in the standard basis, denoted respectively Mstd,1 and Mstd,2 , and the observable corresponding to
measurement of a qubit in the basis {|+i, |−i}, denoted M+− .

3.1 Teleportation
Once upon a time, there were two friends, Alice and Bob who had to separate
and live away from each other. Before leaving, each one took a qubit of the same
EPR pair. Then Bob went very far away, to a place that Alice did not know. Later
on, someone gave Alice a mysterious qubit in a state |ψi = α|0i + β|1i, with a
mission to forward this state to Bob. Alice could neither meet Bob and give him
the qubit, nor clone it and broadcast copies everywhere, nor obtain information
about α and β. Nevertheless, Alice succeeded thanks to the EPR pair and the
teleportation protocol [4]:
BuildEPR

Alice

def

=

def

=

[ x : Qubit, y : Qubit .
((g1 ?x .g2 ?y .H[x].CN ot[x, y].end)
k (g1 !0 .g2 !0 .end))\{g1 , g2 }
]

[ x : Qubit, y : Qubit .
CN ot[x, y].H[x].meas !Mstd,2 [x, y] .end
]

9

Bob

def

=

Teleport

[ z : Qubit .
[ k : Nat .
meas ?k .
[ k = 0 → I[z].end,
k = 1 → X[z].end,
k = 2 → Z[z].end,
k = 3 → Y [z].end ]
]
]
def

=

[ ψ : Qubit .
[ a : Qubit, b : Qubit .
BuildEPR[a, b] ;
(Alice[ψ, a] k Bob[b])\{meas}
]
]

The inference rules can be used to show that this protocol results in Bob’s z
qubit having the state initially possessed by the x qubit of Alice, with only two
classical bits sent from Alice to Bob.

3.2

Communication protocols

Alice sends qubits to Bob through a non secure channel and Eve eavesdrops this
channel to get information on the qubits sent by Alice. In the following example
A, B, and E are processes modeling whatever Alice, Bob, and Eve may respectively apply to their qubits. The actions of these processes, which are not made
explicit here, will be specified in the next example of the BB84 protocol.
The communication protocols which are described here could be used to model cryptographic protocols so as to check if they are secure.

Eve intercepts all qubits
Eve intercepts qubits because of a flaw in the channel that Alice and Bob are using
to communicate.
Alice

def

=

[ a : Qubit . A[a] ; fill !a .end ] ; Alice

10

Bob
Eve

Flaw

def

=

[ b : Qubit . empty ?b .B[b] ] ; Bob

def

[ e : Qubit, f : Qubit .
emptyFlaw ?e .E[e, f ] ; fillFlaw !f .end
] ; Eve

=

def

=

Channel

Protocol

[ u : Qubit, v : Qubit . emptyFlaw !u .fillFlaw ?v .end ]
def

=

[ x : Qubit, y : Qubit . fill ?x .Flaw[x, y] ; empty !y .end ] ;
Channel

def

(Alice k Bob k Eve k Channel)
\{ fill, empty, fillFlaw, emptyFlaw}

=

Eve intercepts some of the qubits
This part assumes that a nondeterministic process composition P +Q is introduced
in the process algebra. This operator is not presented in the operational semantics
in appendix A.2 but it can be simulated by [ true → P, true → Q ] .
To model the fact that Eve does not succeed in intercepting all qubits, the flaw
in the channel is made nondeterministic:
Channel

def

=

[ x : Qubit .
fill ?x .
(
[ y : Qubit . Flaw[x, y] ; empty !y .end ] +
(empty !x .end)
)
] ; Channel

3.3 The BB84 protocol
The BB84 protocol [3] is a protocol for secure quantum key distribution: Alice
and Bob must agree on a private key, i.e. a list of bits that should remain secret.
To communicate, they send qubits through a non secure channel. In fact, the
processes A and B left unspecified in the previous paragraph can be used to model
this protocol. The process Alice is redefined and the process B used by Bob is
made explicit. In addition, another process is defined: the process Random which
11

initializes a bit randomly at 0 or 1. The gates keepDataA and keepDataB are used
by Alice and Bob respectively to send the bits that they want to keep.
def

=

Alice

Random

A1

A2

[ a : Qubit, dataA : Nat, baseA : Nat .
A1 [a, dataA, baseA] ; fill !a .A2 [dataA, baseA]
] ; Alice
def

=

[ r : Nat .
[ x : Qubit .
(g !0 .end k g ?x .end)\{g} ;
H[x].
(h !Mstd,1 [x] .end k h ?r .end)\{h}
]
]

def

=

[ a : Qubit, dataA : Nat, baseA : Nat .
Random[dataA][a] ;
Random[baseA] ;
[ baseA = 1 → H[a].end ]
]

def

[ dataA : Nat, baseA : Nat .
[ bool : Nat, ok : Nat .
received ?ok .
base !baseA .
keep ?bool .
[ bool = 1 → keepDataA !dataA .end ]
]
]

=

12

B

4

def

=

[ b : Qubit .
[ baseA : Nat, baseB : Nat, dataB : Nat .
Random[baseB] ;
(
[ baseB = 0 → g !Mstd,1 [b] .end,
baseB = 1 → g !M+− [b] .end ]
k g ?dataB .end
)\{g} ;
received !1 .
base ?baseA .
[ baseA = baseB → keep !1 .keepDataB !dataB .end,
baseA 6= baseB → keep !0 .end ]
]
]

Probabilistic branching bisimulation

The operational semantics associates a process graph with a process state. A process graph is a graph where vertices are process states and edges are transitions
labeled with actions or probabilities. Each process graph has an initial state.
A bisimulation is an equivalence relation on process states. It identifies states
when they are associated with process graphs having the same branching structure.
The bisimulation defined here is probabilistic because of probabilities introduced by quantum measurement and branching because some transitions are considered as silent. It is inspired from the definitions in [8] and [1].

4.1

Preliminary definitions and notations

Process states
The set of all possible process states is denoted S. Let S, T ∈ S, then S can be
written P/CP and T , Q/CQ where P , Q are process terms and CP , CQ contexts
(possibly probabilistic).
Assuming that S = P/CP and CP =< s, q = ρ, f >, if x is a qubit in S
and x ∈ q, then ρSx is the state of x and this state can be obtained with a trace out
operation on ρ:
ρSx = T r{x}/q (ρ)

13

Silent transitions
τ

The transitions considered as silent are of course internal transitions ( −→ ) but
also probabilistic transitions. The reason is that we want, for example, the following states S1 and S2 to be equivalent.
S2
S1

0.2

✠
a
❄
T

a
❄
T

Silent transitions will be denoted
empty) of silent transitions.

.

∗

❅
0.8
❅
❘
❅
a
❄
T

stands for a sequence (possibly

Function µ
Probabilistic transitions are considered silent, nonetheless, in two equivalent states, the corresponding actions that can be performed on both sides must occur with
the same probability.
Let ≡ be an equivalence on process states, S be a process state and S̄, its
equivalence class with respect to ≡. If M is a set of process states and S a state,
then S ⊲ M means that there exists a sequence of transitions remaining in M ∪ S̄,
from S to a state of M .
A function µ≡ : S × P(S) → [0, 1] is defined for computing the probability to
reach a state in the set M from a state S without leaving S̄ ∪M . It should be noted
that, for this function to yield a probability, nondeterminism must be eliminated
in a way which allows the computation of µ. Here, nondeterminism is treated as
equiprobability, but this is just a convention for the definition of µ≡ . For example,
it does not imply the equivalence of the following two process states:
S2
S1
a ❅ a
❅
✠
❘
❅
T
T

0.5

✠
a
❄
T

14

❅
0.5
❅❅
❘
a
❄
T

A bisimulation is an equivalence relation ≡ which must verify some properties, among which: if S ≡ T then µ≡ (S, M ) = µ≡ (T, M ) for all M equivalence
class of ≡. In this case, µ≡ (S, M ) is the probability to perform an action.
The function µ≡ is defined by:
• if S ∈ M then µ≡ (S, M ) = 1
• else if ∃ T ∈ M ∪ S̄ such that S −→p T ⊲ M
then let ES = {R ∈ M ∪ S̄ | S −→pR R ⊲ M }
in
X
µ≡ (S, M ) =
pR µ≡ (R, M )

S

p3

T1

T2
a

• else if ∃ T ∈ M ∪ S̄ such thataS −→ T ⊲ M
R
then let ES = {R ∈ M ∪ S̄ | S −→
R ⊲ M } in
1
|ES |

T3

p2

R∈ES

µ≡ (S, M ) =

S

E S p1

X

S
ES

µ≡ (R, M )

a

T1

M

S
c

b

T3

R∈ES

T2

M

• else µ≡ (S, M ) = 0
Equivalence of contexts
Let σ be a renaming on variables. The extensions of σ to environment stacks and
sequences of quantum variables are also called σ.
Let C =< s, q = ρ, f > and C ′ =< s′ , q ′ = ρ′ , f ′ > be two contexts, C and
′
C are equivalent, if and only if there exists a renaming σ such that:
• σ(s) = s′
• ∃ a permutation π such that π(σ(q)) = q ′ and π(ρ) = ρ′
• ∀x ∈ dom(f ), σ(x) ∈ dom(f ′) and f (x) = f ′ (σ(x))
• ∀y ∈ dom(f ′), σ −1 (y) ∈ dom(f ) and f (σ −1 (y)) = f ′ (y)
This equivalence relation can easily be extended to probabilistic contexts.

15

4.2

Probabilistic branching bisimulation: definition

An equivalence relation is a probabilistic branching bisimulation if and only if:
•

if S and T are equivalent and if an action a can be performed from S, then the
same action can performed from T , possibly after several silent transitions;
′

T
S
a

′′

•

the reached states (S and T ) are equivalent;

•

the action a must occur with the same
probability in both cases.

S’

T’

*
a

T’’

Let ≡ be an equivalence relation on process states. ≡ is a probabilistic branching bisimulation if and only if it satisfies:
• Termination
δ

if S ≡ T and S −→ S ′ then
δ
∗
∃ T ′ , T ′′ such that (T
T ′ −→ T ′′ ∧ S ≡ T ′ ∧ S ′ ≡ T ′′ ) and the
′
′′
contexts in S and T are equivalent
• Value sending
g !v

if S ≡ T and S −→ S ′ (v classical value) then
g !v
∃ T ′ , T ′′ such that (T ∗ T ′ −→ T ′′ ∧ S ≡ T ′ ∧ S ′ ≡ T ′′ )
• Qubit sending
g !x

if S ≡ T and S −→ S ′ (x variable) then
g !y
∃ T ′ , T ′′ such that (T ∗ T ′ −→ T ′′ ∧ ρSx = ρTy ∧ S ≡ T ′ ∧ S ′ ≡ T ′′ )
• Value reception
g ?v

if S ≡ T and S −→ S ′ (v classical value) then
g ?v
∃ T ′ , T ′′ such that (T ∗ T ′ −→ T ′′ ∧ S ≡ T ′ ∧ S ′ ≡ T ′′ )
• Qubit reception
g ?x

if S ≡ T and S −→ S ′ (x variable) then
′
′′
g ?y
∃ T ′ , T ′′ such that (T ∗ T ′ −→ T ′′ ∧ ρSx = ρTy ∧ S ≡ T ′ ∧ S ′ ≡ T ′′ )

16

• Silent transition
if S ≡ T and S

S ′ then S ′ ≡ T

• Probabilities
if S ≡ T then µ≡ (S, M ) = µ≡ (T, M ), ∀M ∈ (S/ ≡)\{S̄}

4.3

Bisimulation and recursion

Recursion in a process definition introduces circuits in the associated process
graph. As a consequence, it must be proved that in this case, the notion of probabilistic branching bisimulation is well-defined. In fact, the only point that could
be a problem is the definition of µ≡ .
Let S be a process state and M be a set of process states, the computation of
µ≡ (T, M ) for all T in S̄ leads to a linear system of equations where the µ≡ (T, M )
are the unknowns:
X = AX + B
The ith row in this system can be written: xi = ai1 x1 + · · · + ain xn + bi .
The coefficients aij and bi are either probabilities or average coefficients in
the case of nondeterminism. As a consequence: 0 ≤ aij ≤ 1 and 0 ≤ bi ≤ 1.
Moreover, in the definition of µ≡ , every state in the set ES is such that there exists
a path from that state to the set M . Therefore, the system of equations obtained
can be transformed into a system such that bi > 0, ∀i ∈ J1, nK. From now on, we
consider that the system verifies this property.
P
P
Another property of the system is: 0 ≤ j aij +bi ≤ 1, thus 0 ≤ j aij < 1.
To prove that the system has a unique solution, it is sufficient to prove kAk < 1
and use the fixpoint theorem. The norms for matrices and vectors are:
kAk = sup kAXk

kXk = max |xi |
i

kXk=1

We obtain:
kAXk = max |
i

X

aij xi | ≤ max
i

j

and then kAk ≤ max
i

X

X

(|aij ||xi |)

j

|aij | < 1

j

kAk < 1 implies that the function f : X 7→ AX + B is strictly contracting, so
from the fixpoint theorem, we infer that the equation X = AX + B has a unique
solution. Moreover, as f ([0, 1]) ⊆ [0, 1], this solution belongs to [0, 1].
As a consequence, the function µ≡ is well-defined even in case of recursive
processes.
17

5

Conclusion

This paper has presented a process algebra for quantum programming which can
describe both classical and quantum programming, and their cooperation. Without this cooperation, the implementation of protocols like BB84 is not possible.
Another feature of this language is that measurement and initialization of quantum
registers occur through communications between quantum and classical parts of
the language, which happens to be a faithful model of physical reality.
Moreover, a thorough semantics has been defined, thus allowing the study
and analysis of programs. One peculiarity of this semantics is the introduction
of probabilistic processes, due to quantum measurement. Probabilistic processes
perform probabilistic transitions. As a consequence, the execution tree obtained
from a process presents action branches and probabilistic branches.
Finally a semantical equivalence relation on processes has been defined. This
equivalence is a bisimulation which identifies processes associated with process
graphs having the same branching structure. This is the first step toward the verification of quantum cryptographic protocols.
Several extensions are possible. As already mentioned, a nondeterministic
process composition operator can be introduced. A probabilistic composition of
processes could be added. This would allow, for example, the description of communication protocols in which Eve intercepts qubits with a given probability.

References
[1] S. Andova. Process algebra with probabilistic choice. Lecture Notes in
Computer Science, 1601:111–129, 1999.
[2] P. Arrighi and G. Dowek. Operational semantics for formal tensorial calculus. Proceedings of The 2nd International Workshop on Quantum Programming Languages, pages 21 – 38, July 2004.
[3] C. H. Bennett and G. Brassard. Quantum cryptography: Public-key distribution and coin tossing. In Proceedings of the IEEE International Conference
on Computer, Systems and Signal Processing, pages 175–179, Bangalore,
India, December 1984.
[4] C. H. Bennett, G. Brassard, C. Crépeau, R. Jozsa, A. Peres, and W. Wootters.
Teleporting an unknown quantum state via dual classical and EPR channels.
Physical Review Letters, 70:1895–1899, 1993.

18

[5] T. Bolognesi and E. Brinksma. Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems, 14(1):25–59, 1987.
[6] D. Cazorla, F. Cuartero, V. Valero, and F. L. Pelayo. A process algebra
for probabilistic and nondeterministic processes. Information Processing
Letters, 80(1):15–23, 2001.
[7] D. Cazorla, F. Cuartero, V. Valero, F. L. Pelayo, and J. Pardo. Algebraic
theory of probabilistic and nondeterministic processes. The Journal of Logic
and Algebraic Programming, 55(1–2):57–103, 2003.
[8] W. Fokkink. Introduction to Process Algebra. Springer, 2000.
[9] M. Lalire and Ph. Jorrand. A process algebraic approach to concurrent
and distributed quantum computation: operational semantics. Proceedings
of The 2nd International Workshop on Quantum Programming Languages,
pages 109 – 126, July 2004.
[10] R. Milner. Communication and Concurrency. Prentice-Hall, London, 1999.
[11] R. Nagarajan and S. Gay. Communicating quantum processes. Proceedings
of The 2nd International Workshop on Quantum Programming Languages,
pages 91 – 107, July 2004.
[12] B. Omer. Quantum programming in QCL. Master’s thesis, Institute Information System, Technical University of Vienna, 2000.
[13] P. Selinger. Towards a quantum programming language. To appear in Mathematical Structures in Computer Science, 2003.
[14] A. Van Tonder. A lambda calculus for quantum computation. Los Alamos
arXive e-print quant-ph/0307150, 2003.
[15] P. Zuliani. Quantum Programming. PhD thesis, St Cross College, University
of Oxford, 2001.

19

A

The quantum process algebra

A.1 Syntax
process

::=
|
|
|
|
|
|
|
|

nil
end
action . process
process ; process
process k process
process \{ gate list }
[ cond list ]
[ var decl list . process ]
process name [[[ var list ] ]

action

::=
|
|

communication
unit transf
measurement

communication

::=
|
|

gate ! exp
gate ! measurement
gate ? variable

unit transf

::=

unitary operator [ var list ]

measurement

::=

observable [ var list ]

var decl

::=

variable : var type

proc def

::=

process name = process

def

A.2 Main inference rules of the semantics
The semantics is specified with inference rules which give the evolution of the
states of processes. There are four kinds of transitions:
α

• action transition: −→ where α is g !x or g ?x ;
τ

• silent transition: −→ , for internal transition;
δ

• delta transition: −→ , for successful termination;

20

• probabilistic transition: −→p , where p is a probability.
In the following, P, Q, P ′ , Q′ , Pi and Pi′ are processes, C, C ′ and Ci are
contexts, α is an action, g is a communication gate, v is a value, x is a variable,
and cj is a condition.
Successful termination
end/C

−−δ−→ nil/C

C↓

Action Prefix
g !v .P/C

g !v
P/C
−−−−−−→

v ∈ IN, C ↓

g !x .P/C

g !f (x)
P/C
−−−−−−−−→
where C =< s, q = ρ, f >, x ∈ Var(s) and x ∈ dom(f )
g !x .P/C

g !x
−−−−−−→

P/C ′

where
• C =< s, q = ρ, f >, C ′ =< s\{x}, q\{x} = T r{x}/q (ρ), f >
• x ∈ Var(s) and x ∈ q
g ?x .P/C

g ?v
P/C ′
−−−−−−→

where
• C =< s, q = ρ, f >, C ′ =< s, q = ρ, f ∪ {x 7→ v} >
• x ∈ Var(s), x of type Nat, v ∈ IN
g ?x .P/C

g ?x
P/C ′
−−−−−−→

where
• C =< s, q = ρ, f >, C ′ =< s, x.q = ν ⊗ ρ, f >
• x ∈ Var(s), x of type Qubit, x 6∈ q
21

• ν density matrix of dimension 2
U [x1 , . . . , xn ].P/C

′
−−τ−→ P/C

where
• C =< s, q = ρ, f >, C ′ =< s, q = ρ′ , f >
• U ∈ U, x1 , . . . , xn ∈ Var(s), and x1 , . . . , xn ∈ q
• ∀ i, j ∈ {0, . . . , n} such that i 6= j : xi 6= xj
• ρ′ = TU (ρ)
T is defined in the following way: if A is a 2n × 2n matrix, then
TA : ρ 7→ Π† .(A ⊗ I ⊗k ).Π.ρ.Π† .(A† ⊗ I ⊗k ).Π
where Π is the permutation matrix which places the xi ’s at the head of q, and
k = size(q) − n .

M [x1 , . . . , xn ].P/ < s, q = ρ, f >

−−τ−→ P/ < s, q = ρ, f >

with
• x1 , . . . , xn ∈ Var(s) and x1 , . . . , xn ∈ q
• ∀ i, j ∈ {0, . . . , n} such that i 6= j : xi 6= xj
P
• M ∈ O with i λi Pi as spectral decomposition
P
• ρ′ = i TPi (ρ)
g !M [x1 , . . . , xn ] .P/C

−−τ−→ [ g !y .end ] ; P/ ⊞pi Ci

where
• C =< s, q = ρ, f > (which implies C ↓)
• Ci =< {(y, Nat)}.s, q = ρi , f ∪ {y 7→ λi } >
• x1 , . . . , xn ∈ Var(s) and x1 , . . . , xn ∈ q
22

• ∀ i, j ∈ {0, . . . , n} such that i 6= j : xi 6= xj
• y is a new variable
P
• M ∈ O with i λi Pi as spectral decomposition
• pi = T r(TPi (ρ)),

ρi =

1
pi TPi (ρ)

Probabilistic contexts
P/ ⊞pi Ci

−→pj

P/Cj

where

X

pi = 1

i

Sequential composition
P/C
P ; Q/C

α
P ′ /C ′
−−−→
′
′
−−α
−→ P ; Q/C

α 6= δ

′
′
−−δ−→ P /C
P ; Q/C −−τ−→ Q/C ′

P/C

Parallel composition
In the rules for parallel composition, C, CP and CQ are defined as:
• C =< (sP k sQ ).s, q = ρ, f >
• CP =< sP |s, q = ρ, f >
• CQ =< sQ |s, q = ρ, f >
In the definition of C, the operator k permits to build a cactus stack (see paragraph 2.1). In the cactus stack (sP k sQ ).s of the process P k Q, the names in s
correspond to variables shared by P and Q whereas the names in sP (resp. sQ )
correspond to variables declared in P (resp. Q).
P/CP
P k Q/C

′
′
−−α
−→ P /CP
α
P ′ k Q/C ′
−−−→

α 6= δ

where
• If CP′ =< s′ , q ′ = ρ′ , f ′ > then C ′ =< (s′P k sQ ).s, q ′ = ρ′ , f ′ > with
s′P such that s′ = s′P |s (P can neither add to nor remove variables from s)
23

• If CP′ = ⊞pi < s′i , qi′ = ρ′i , fi′ > then C ′ = ⊞pi < (sP ′i k sQ ).s, qi′ =
ρ′i , fi′ > with sP ′i such that s′i = sP ′i |s
′
g !v
P ′ /CP′
Q/CQ
g ?v
Q′ /CQ
−−−−−−→
−−−−−−→
P k Q/C
τ
P ′ k Q′ /C ′
−−−→
′
where v ∈ IN , CQ
=< s′ , q ′ = ρ′ , f ′ >, and C ′ =< (sP k sQ ).s, q = ρ, f ′ >

P/CP

P/CP

′
g !v
P ′ /CP′
Q/CQ
g ?x
Q′ /CQ
−−−−−−→
−−−−−−→
P k Q/C −−τ−→ P ′ k Q′ /C ′

where
• x ∈ Var(s) ∪ Var(sQ ), x of type Qubit, x 6∈ q, v ∈ {0, 1}
• C ′ =< (sP k sQ ).s, x.q = |vihv| ⊗ ρ, f >
P/CP

′
g !x
P ′ /CP′
Q/CQ
g ?y
Q′ /CQ
−−−−−−→
−−−−−−→
P k Q/C −−τ−→ P ′ k Q′ /C ′

where
• x ∈ Var(s) ∪ Var(sP ), x ∈ q
• y ∈ Var(s) ∪ Var(sQ ), y 6∈ q, y of type Qubit
• C ′ =< ((sP k sQ ).s)\{x}, q[x ← y] = ρ, f >
′
′
′
Q/CQ −−δ−→ Q′ /CQ
−−δ−→ P /CP
P k Q/C −−δ−→ nil/C ′
with C ′ =< s, q\e = T re/q (ρ), f \e > and e = (Var(sP ) ∪ Var(sQ ))

P/CP

Variable declaration
′
−−τ−→ [ P ] /C
with C =< s, q = ρ, f >, C ′ =< s′ , q = ρ, f >
and s′ = {(x1 , t1 ), . . . , (xn , tn )}.s

[ x1 : t1 , . . . , xn : tn . P ] /C

24

End of scope of variables
′
′
−−α
−→ P /C
α 6= δ
[ P ] /C
α
[ P ′ ] /C ′
−−−→
P/C −−δ−→ P ′ / < e.s, q = ρ, f >

P/C

[ P ] /C

−−δ−→ nil / < s, q\Var(e) = T rVar(e)/q (ρ), f \Var(e) >

25

