Formal Analysis of Quantum Systems using Process Calculus

TL;DR

This paper advocates for applying formal methods, like process calculus, to analyze quantum systems, emphasizing the need for rigorous verification techniques in quantum communication and cryptography.

Contribution

It introduces the use of process calculus and behavioral equivalence for formal analysis of quantum systems, bridging a gap in existing verification approaches.

Findings

Initial investigation shows behavioral equivalence can model quantum protocols.

Formal methods can improve correctness proofs for quantum-classical systems.

Highlights the importance of compositional analysis in quantum system verification.

Abstract

Quantum communication and cryptographic protocols are well on the way to becoming an important practical technology. Although a large amount of successful research has been done on proving their correctness, most of this work does not make use of familiar techniques from formal methods, such as formal logics for specification, formal modelling languages, separation of levels of abstraction, and compositional analysis. We argue that these techniques will be necessary for the analysis of large-scale systems that combine quantum and classical components, and summarize the results of initial investigation using behavioural equivalence in process calculus. This paper is a summary of Simon Gay's invited talk at ICE'11.