Verification of Linear Optical Quantum Computing using Quantum Process Calculus

Sonja Franke-Arnold, Simon J. Gay, Ittop Puthoor

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

Abstract

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.
Original languageEnglish
Title of host publicationProceedings of Combined 21st International Workshop on Expressiveness in Concurrency and 11th Workshop on Structural Operational Semantics
EditorsJohannes Borgström, Silvia Crafa
Pages111-129
Volume160
DOIs
Publication statusPublished - 2014

Publication series

NameElectronic Proceedings in Theoretical Computer Science
Volume160

Fingerprint Dive into the research topics of 'Verification of Linear Optical Quantum Computing using Quantum Process Calculus'. Together they form a unique fingerprint.

  • Cite this

    Franke-Arnold, S., Gay, S. J., & Puthoor, I. (2014). Verification of Linear Optical Quantum Computing using Quantum Process Calculus. In J. Borgström, & S. Crafa (Eds.), Proceedings of Combined 21st International Workshop on Expressiveness in Concurrency and 11th Workshop on Structural Operational Semantics (Vol. 160, pp. 111-129). (Electronic Proceedings in Theoretical Computer Science; Vol. 160). https://doi.org/10.4204/EPTCS.160.10