Formal verification of higher dimensional quantum protocols

TL;DR

This paper explores the use of formal methods, specifically quantum process calculus, to model and verify higher dimensional quantum protocols like teleportation and superdense coding, extending previous work to qudits.

Contribution

It extends the theory of behavioural equivalence in CQP to verify higher dimensional quantum protocols using qudits, advancing quantum formal verification methods.

Findings

Preliminary results on extending behavioural equivalence in CQP

Modeling of higher dimensional quantum protocols in CQP

Verification of protocol correctness through behavioural equivalence

Abstract

Formal methods have been a successful approach for modelling and verifying the correctness of complex technologies like microprocessor chip design, biological systems and others. This is the main motivation of developing quantum formal techniques which is to describe and analyse quantum information processing systems. Our previous work demonstrates the possibility of using a quantum process calculus called Communicating Quantum Processes (CQP) to model and describe higher dimensional quantum systems. By developing the theory to generalise the fundamental gates and Bell states, we have modelled quantum qudit protocols like teleportation and superdense coding in CQP. In this paper, we demonstrate the use of CQP to analyse higher dimensional quantum protocols. The main idea is to define two processes, one modelling the real protocol and the other expressing a specification, and prove that they are behaviourally equivalent. This is a work-in-progress and we present our preliminary results in extending the theory of behavioural equivalence in CQP to verify higher dimensional quantum protocols using qudits.