2012/07/03 by Francesco Belardinelli, F. Belardinelli, P. Gonzalez +3
Computer Science · Physics and Astronomy · #Compiler #Computation #Computer science #Distributed computing #Formal verification #Formalism (music) #Logic, Reasoning, and Knowledge #Model checking #Physics #Programming language #Protocol (science) #Quantum #Quantum Computing Algorithms and Architecture #Quantum Mechanics and Applications #Quantum computer #Quantum mechanics #Theoretical computer science #cs.CR #cs.LO #cs.MA #quant-ph
paper · pdf · doi:10.4204/eptcs.85.4
published as EPTCS 85, 2012, pp. 48-62 · In Proceedings QAPL 2012, arXiv:1207.0559
openalex publication_date 2012/07/03 · arxiv created 2012/07/04 · arxiv updated 2012/07/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
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.