Ardeshir-Larijani, E.; Gay, S.; Nagarajan, R.

Equivalence checking of quantum protocols

Book chapter

Ardeshir-Larijani, E., Gay, S. and Nagarajan, R. 2013. Equivalence checking of quantum protocols. in: Piterman, N. and Smolka, S. (ed.) Tools and Algorithms for the Construction and Analysis of Systems : 19th International Conference Proceedings (TACAS 2013). Berlin Springer.

ISBN
Chapter title	Equivalence checking of quantum protocols
Authors	Ardeshir-Larijani, E., Gay, S. and Nagarajan, R.
Abstract	Quantum Information Processing (QIP) is an emerging area at the intersection of physics and computer science. It aims to establish the principles of communication and computation for systems based on the theory of quantum mechanics. Interesting QIP protocols such as quantum key distribution, teleportation, and blind quantum computation have already been realised in the laboratory and are now in the realm of mainstream industrial applications. The complexity of these protocols, along with possible inaccuracies in implementation, demands systematic and formal analysis. In this paper, we present a new technique and a tool, with a high-level interface, for verification of quantum protocols using equivalence checking. Previous work by Gay, Nagarajan and Papanikolaou used model-checking to verify quantum protocols represented in the stabilizer formalism, a restricted model which can be simulated efficiently on classical computers. Here, we are able to go beyond stabilizer states and verify protocols efficiently on all input states.
Research Group	Foundations of Computing group
Book title	Tools and Algorithms for the Construction and Analysis of Systems : 19th International Conference Proceedings (TACAS 2013).
Editors	Piterman, N. and Smolka, S.
Publisher	Springer
Place of publication	Berlin
Series	Lecture Notes in Computer Science
Hardcover	9783642367410
ISSN	0302-9743
Publication dates
Print	2013
Publication process dates
Deposited	05 Jul 2013
Output status	Published
Additional information	Conference: TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013.
Digital Object Identifier (DOI)	https://doi.org/10.1007/978-3-642-36742-7_33
Language	English

Permalink -

https://repository.mdx.ac.uk/item/842xv

Log in to edit

65
total views
0
total downloads
1
views this month
0
downloads this month

Export as

Related outputs

Formalizing federated learning and differential privacy for GIS systems in IIIf

Kammueller, F., Piras, L., Fields, B. and Nagarajan, R. 2024. Formalizing federated learning and differential privacy for GIS systems in IIIf. 3rd International Workshop on System Security Assurance. Bydgoszcz, Poland 19 - 20 Sep 2024 Springer.

Describing and simulating concurrent quantum systems

Bornat, R., Boender, J., Kammueller, F., Poly, G. and Nagarajan, R. 2020. Describing and simulating concurrent quantum systems. Biere, A. and Parker, D. (ed.) International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 20). Dublin 27 - 30 Apr 2020 Springer. pp. 271-277 https://doi.org/10.1007/978-3-030-45237-7_16

Automated equivalence checking of concurrent quantum systems

Ardeshir-Larijani, E., Gay, S. and Nagarajan, R. 2018. Automated equivalence checking of concurrent quantum systems. ACM Transactions on Computational Logic. 19 (4), pp. 1-32. https://doi.org/10.1145/3231597

Quantum error-correcting output codes

Windridge, D., Mengoni, R. and Nagarajan, R. 2018. Quantum error-correcting output codes. International Journal of Quantum Information. 16 (8). https://doi.org/10.1142/S0219749918400038

A proof-theoretic trust and reputation model for VANET

Primiero, G., Raimondi, F., Chen, T. and Nagarajan, R. 2017. A proof-theoretic trust and reputation model for VANET. S4CIP’17: 2nd Workshop on Safety & Security aSSurance for Critical Infrastructures Protection. Paris, France 29 Apr 2017 Institute of Electrical and Electronics Engineers (IEEE). pp. 146-152 https://doi.org/10.1109/EuroSPW.2017.64

Quantum Bootstrap Aggregation

Windridge, D. and Nagarajan, R. 2017. Quantum Bootstrap Aggregation. de Barros, J., Coecke, B. and Pothos, E. (ed.) Quantum Interaction. San Francisco, CA, USA 20 - 22 Jul 2016 Springer. pp. 115-121 https://doi.org/10.1007/978-3-319-52289-0_9

Hamming distance kernelisation via topological quantum computation

Di Pierro, A., Mengoni, R., Nagarajan, R. and Windridge, D. 2017. Hamming distance kernelisation via topological quantum computation. Martín-Vide C., Neruda R. and Vega-Rodríguez M. (ed.) 6th International Conference on the Theory and Practice of Natural Computing. Prague, Czech Republic 18 - 20 Dec 2017 Springer. pp. 269-280 https://doi.org/10.1007/978-3-319-71069-3_21

Techniques for formal modelling and analysis of quantum systems

Gay, S. and Nagarajan, R. 2013. Techniques for formal modelling and analysis of quantum systems. in: Computation, logic, games, and quantum foundations. The many facets of Samson Abramsky Springer Verlag.

Formalization of quantum protocols using Coq

Boender, J., Kammueller, F. and Nagarajan, R. 2015. Formalization of quantum protocols using Coq. The 12th International Workshop on Quantum Physics and Logic (QPL 2015). Oxford, United Kingdom 15 - 17 Jul 2015 pp. 71-83

Verification of quantum protocols using Coq

Boender, J., Kammueller, F. and Nagarajan, R. 2014. Verification of quantum protocols using Coq. 17th Conference on Quantum Information Processing (QIP). Barcelona, Spain 03 - 07 Feb 2014

Verification of concurrent quantum protocols by equivalence checking

Ardeshir-Larijani, E., Gay, S. and Nagarajan, R. 2014. Verification of concurrent quantum protocols by equivalence checking. TACAS 2014: 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Grenoble, France 05 - 13 Apr 2014 Springer. https://doi.org/10.1007/978-3-642-54862-8_42