Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formal verification of higher dimensional quantum protocols

Ittoop Vergheese Puthoor

TL;DR

This work extends quantum formal methods to higher-dimensional systems by deploying Communicating Quantum Processes (CQP) to model qudit-based protocols and verify them via behavioural equivalence against high-level specifications. It advances the theory by defining probabilistic branching bisimulation for qudits, incorporating density-matrix reasoning, mixed configurations, and congruence properties to compare concrete protocols with specifications. A central case study is qudit teleportation, modeled in CQP as a pair of processes with entangled qudits and corrective actions, and shown to be bisimilar to a high-level spec $QWire$ in principle. The findings lay groundwork for formally verifying a broader class of qudit protocols and motivate future work on additional protocols, realistic physical implementations, and automated verification tooling.

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.

Formal verification of higher dimensional quantum protocols

TL;DR

This work extends quantum formal methods to higher-dimensional systems by deploying Communicating Quantum Processes (CQP) to model qudit-based protocols and verify them via behavioural equivalence against high-level specifications. It advances the theory by defining probabilistic branching bisimulation for qudits, incorporating density-matrix reasoning, mixed configurations, and congruence properties to compare concrete protocols with specifications. A central case study is qudit teleportation, modeled in CQP as a pair of processes with entangled qudits and corrective actions, and shown to be bisimilar to a high-level spec in principle. The findings lay groundwork for formally verifying a broader class of qudit protocols and motivate future work on additional protocols, realistic physical implementations, and automated verification tooling.

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.
Paper Structure (10 sections, 2 theorems, 14 equations, 3 figures)

This paper contains 10 sections, 2 theorems, 14 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Background
  3. Modelling quantum protocols in process calculus
  4. Teleportation
  5. Behavioural Equivalence of CQP Processes
  6. Correctness of $Teleport$
  7. Conclusion and Future Work
  8. Appendix
  9. Syntax
  10. Semantics

Key Result

Theorem 1

If $P \leftrightarroweq^c Q$ then for any context ${C}[]$, if ${C}[P]$ and ${C}[Q]$ are typable then ${C}[P] \leftrightarroweq^c {C}[Q]$.

Figures (3)

  • Figure 1: Teleportation of qudit $|\psi\rangle$
  • Figure 2: Syntax of CQP.
  • Figure 3: Internal syntax of CQP.

Theorems & Definitions (8)

  • Definition 1: Density Matrix of Configurations
  • Definition 2: Probabilistic Branching Bisimulation
  • Definition 3: Probabilistic Branching Bisimilarity
  • Definition 4: Probabilistic Branching Bisimilarity of Processes
  • Definition 5: Full probabilistic branching bisimilarity
  • Theorem 1: Full probabilistic branching bisimilarity is a congruence
  • proposition thmcounterproposition
  • proof