Techniques for formal modelling and analysis of quantum systems

Book chapter

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.
Chapter titleTechniques for formal modelling and analysis of quantum systems
AuthorsGay, S. and Nagarajan, R.
Abstract

Quantum communication and cryptographic protocols are well on the way to becoming an important practical technology. Although a large amount of successful research has been done on proving their correctness, most of this work does not make use of familiar techniques from formal methods such as formal logics for specification, formal modelling languages, separation of levels of abstraction, and compositional analysis. We argue that these techniques will be necessary for the analysis of large-scale systems that combine quantum and classical components. We summarize the results of our investigation using different approaches: behavioural equivalence in process calculus, model-checking and equivalence checking. Quantum teleportation is used as an example to illustrate our techniques.

Book titleComputation, logic, games, and quantum foundations. The many facets of Samson Abramsky
PublisherSpringer Verlag
ISSN0302-9743
Publication dates
Print2013
Publication process dates
Deposited09 Jun 2015
Output statusPublished
Digital Object Identifier (DOI)https://doi.org/10.1007/978-3-642-38164-5_18
LanguageEnglish
Permalink -

https://repository.mdx.ac.uk/item/85963

Log in to edit
  • 58
    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. 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
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.
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.