Imperial College London

ProfessorAlessioLomuscio

Faculty of EngineeringDepartment of Computing

Professor of Logic for Multiagent Systems
 
 
 
//

Contact

 

+44 (0)20 7594 8414a.lomuscio Website

 
 
//

Location

 

504Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Belardinelli:2012:10.4204/EPTCS.85.4,
author = {Belardinelli, F and Gonzalez, P and Lomuscio, A},
doi = {10.4204/EPTCS.85.4},
pages = {48--62},
publisher = {arXiv},
title = {Automated verification of quantum protocols using MCMAS},
url = {http://dx.doi.org/10.4204/EPTCS.85.4},
year = {2012}
}

RIS format (EndNote, RefMan)

TY  - CPAPER
AB - 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.
AU - Belardinelli,F
AU - Gonzalez,P
AU - Lomuscio,A
DO - 10.4204/EPTCS.85.4
EP - 62
PB - arXiv
PY - 2012///
SP - 48
TI - Automated verification of quantum protocols using MCMAS
UR - http://dx.doi.org/10.4204/EPTCS.85.4
UR - https://arxiv.org/abs/1207.1271v1
UR - http://hdl.handle.net/10044/1/64909
ER -