Automated Verification of Quantum Protocols using MCMAS
F. Belardinelli (Imperial College London), P. Gonzalez (Imperial, College London), A. Lomuscio (Imperial College London)
TL;DR
This paper introduces an automated method for verifying quantum protocols by translating distributed measurement-based quantum computation models into a form suitable for symbolic model checking with MCMAS, enabling formal analysis of quantum systems.
Contribution
It develops a translation from distributed measurement-based quantum computation models to interpreted systems for model checking, and implements a compiler for verifying quantum protocols with MCMAS.
Findings
Successfully verified the Quantum Teleportation Protocol
Demonstrated the effectiveness of the translation and tool performance
Extended classical model checking techniques to quantum protocols
Abstract
We present a methodology for the automated verification of quantum protocols using MCMAS, a symbolic model checker for multi-agent systems The method is based on the logical framework developed by D'Hondt and Panangaden for investigating epistemic and temporal properties, built on the model for Distributed Measurement-based Quantum Computation (DMC), an extension of the Measurement Calculus to distributed quantum systems. We describe the translation map from DMC to interpreted systems, the typical formalism for reasoning about time and knowledge in multi-agent systems. Then, we introduce dmc2ispl, a compiler into the input language of the MCMAS model checker. We demonstrate the technique by verifying the Quantum Teleportation Protocol, and discuss the performance of the tool.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.