QMC: a model checker for quantum systems

Book chapter


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.
Chapter titleQMC: a model checker for quantum systems
AuthorsGay, S., Nagarajan, R. and Papanikolaou, N.
Abstract

The novel field of quantum computation and quantum information has been growing at a rapid rate; the study of quantum information in particular has led to the emergence of communication and cryptographic protocols with no classical analogues. Quantum information protocols have interesting properties which are not exhibited by their classical counterparts, but they are most distinguished for their applications in cryptography. Notable results include the unconditional security proof [1] of quantum key distribution. This result, in particular, is one of the reasons for the widespread interest in this field. Furthermore, the implementation of quantum cryptography has been demonstrated in non-laboratory settings and is already an important practical technology. Implementations of quantum cryptography have already been commercially launched and tested by a number of companies including MagiQ, Id Quantique, Toshiba, and NEC. The unconditional security of quantum key distribution protocols does not automatically imply the same degree of security for actual systems, of course; this justifies the need for systems modelling and verification in this setting.

Research GroupFoundations of Computing group
Book titleComputer Aided Verification : 20th International Conference, (CAV 2008) Proceedings
EditorsGupta, A. and Malik, S.
PublisherSpringer
Place of publicationBerlin
SeriesLecture Notes in Computer Science
ISBN
Hardcover9783540705437
ISSN0302-9743
Publication process dates
Deposited03 Jul 2013
Output statusPublished
Additional information

Conference took place: Princeton, NJ, USA, July 7-14, 2008

Digital Object Identifier (DOI)https://doi.org/10.1007/978-3-540-70545-1_51
LanguageEnglish
Permalink -

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

  • 41
    total views
  • 0
    total downloads
  • 2
    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 (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
Equivalence checking of quantum protocols
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.