Verification of linear optical quantum computing using quantum process calculus

Sonja Franke‐Arnold, Simon J. Gay, Ittoop Vergheese Puthoor

Ittoop Vergheese Puthoor

Sonja Franke‐Arnold, Simon J. Gay, Ittoop Vergheese Puthoor

We explain the use of quantum process calculus to describe and analyse linear optical quantum computing (LOQC). The main idea is to define two processes, one modelling a linear optical system and the other expressing a specification, and prove that they are behaviourally equivalent. We extend the theory of behavioural equivalence in the process calculus Communicating Quantum Processes (CQP) to include multiple particles (namely photons) as information carriers, described by Fock states or number states. We summarise the theory in this paper, including the crucial result that equivalence is a congruence, meaning that it is preserved by embedding in any context. In previous work, we have used quantum process calculus to model LOQC but without verifying models against specifications. In this paper, for the first time, we are able to carry out verification. We illustrate this approach by describing and verifying two models of an LOQC CNOT gate.

Nicolas Heurtel

Graphical languages are powerful and useful to represent, rewrite and simplify different kinds of processes. In particular, they have been widely used for quantum processes, improving the state of the art for compilation, simulation and verification. In this work, we focus on one of the main carrier of quantum information and computation: linear optical circuits. We introduce the LO_fi-calculus, the first graphical language to reason on the infinite-dimensional photonic space with circuits only composed of the four core elements of linear optics: the phase shifter, the beam splitter, and auxiliary sources and detectors with bounded photon number. First, we study the subfragment of circuits composed of phase shifters and beam splitters, for which we provide the first minimal equational theory. Next, we introduce a rewriting procedure on those LO_fi-circuits that converge to normal forms. We prove those forms to be unique, establishing both a novel and unique representation of linear optical processes. Finally, we complement the language with an equational theory that we prove to be complete: two LO_fi-circuits represent the same quantum process if and only if one can be transformed into the other with the rules of the LO_fi-calculus.

Nobuyuki Matsuda

Christoph Adami, Nicolas J. Cerf