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.
Chapter titleEquivalence checking of quantum protocols
AuthorsArdeshir-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 GroupFoundations of Computing group
LanguageEnglish
Book titleTools and Algorithms for the Construction and Analysis of Systems : 19th International Conference Proceedings (TACAS 2013).
EditorsPiterman, N. and Smolka, S.
PublisherSpringer
Place of publicationBerlin
SeriesLecture Notes in Computer Science
ISBN
Hardcover9783642367410
ISSN0302-9743
Publication dates
Print2013
Publication process dates
Deposited05 Jul 2013
Output statusPublished
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
Permalink -

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

  • 34
    total views
  • 0
    total downloads
  • 1
    views this month
  • 0
    downloads this month

Export as

Related outputs

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 (TOCL). 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
Model checking for communicating quantum processes
Davidson, T., Gay, S., Mlnařík, H., Nagarajan, R. and Papanikolaou, N. 2012. Model checking for communicating quantum processes. International Journal of Unconventional Computing. 8 (1), pp. 73-98.
Lossless quantum prefix compression for communication channels that are always open
Müller, M., Rogers, C. and Nagarajan, R. 2009. Lossless quantum prefix compression for communication channels that are always open. Physical Review A. 79 (1). https://doi.org/10.1103/PhysRevA.79.012302
QMC: a model checker for quantum systems
Gay, S., Nagarajan, R. and Papanikolaou, N. 2008. QMC: a model checker for quantum systems. in: Gupta, A. and Malik, S. (ed.) Computer Aided Verification : 20th International Conference, (CAV 2008) Proceedings Berlin Springer.