Core Concepts
This paper presents preliminary results in extending the theory of behavioral equivalence in the Communicating Quantum Processes (CQP) formalism to verify higher-dimensional quantum protocols using qudits.
Abstract
The paper discusses the use of formal methods, specifically the quantum process calculus CQP, to model and analyze higher-dimensional quantum systems and protocols.
Key highlights:
Quantum technologies, such as quantum computing and cryptography, are complex systems that require rigorous verification techniques.
The authors have previously demonstrated the ability of CQP to model and describe higher-dimensional quantum systems involving qudits.
In this work, the authors focus on extending the theory of behavioral equivalence in CQP to verify higher-dimensional quantum protocols, using the qudit teleportation protocol as a case study.
The paper presents the preliminary definitions and results in extending the concepts of probabilistic branching bisimulation and bisimilarity to analyze qudit protocols.
The authors show that the teleportation protocol modeled in CQP is behaviorally equivalent to a specification process QWire, which describes the high-level observational behavior of the protocol.
The authors note that this work is still in progress, and future work includes extending the analysis to other higher-dimensional protocols and exploring the modeling of realistic higher-dimensional quantum systems.