Techniques for formal modelling and analysis of quantum systems. (English) Zbl 1264.81073
Coecke, Bob (ed.) et al., Computation, logic, games, and quantum foundations. The many facets of Samson Abramsky. Essays dedicated to Samson Abramsky on the occasion of his 60th birthday. Berlin: Springer (ISBN 978-3-642-38163-8/pbk). Lecture Notes in Computer Science 7860, 264-276 (2013).
Summary: 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.
For the entire collection see [Zbl 1263.68015].
For the entire collection see [Zbl 1263.68015].
MSC:
| 81P45 | Quantum information, communication, networks (quantum-theoretic aspects) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 81P94 | Quantum cryptography (quantum-theoretic aspects) |
Software:
QPLReferences:
| [1] | Aaronson, S., Gottesman, D.: Improved simulation of stabilizer circuits. Physical Review A 70, 052328 (2004) · doi:10.1103/PhysRevA.70.052328 |
| [2] | Abramsky, S., Gay, S.J., Nagarajan, R.: Interaction categories and the foundations of typed concurrent programming. In: Broy, M. (ed.) Deductive Program Design: Proceedings of the 1994 Marktoberdorf International Summer School. NATO ASI Series F: Computer and Systems Sciences. Springer (1995) · Zbl 0934.18007 |
| [3] | Abramsky, S.: Interaction Categories (Extended Abstract). In: Burn, G.L., Gay, S.J., Ryan, M.D. (eds.) Theory and Formal Methods 1993: Proceedings of the First Imperial College Department of Computing Workshop on Theory and Formal Methods. Workshops in Computer Science, pp. 57–70. Springer (1993) |
| [4] | Abramsky, S., Coecke, B.: A categorical semantics of quantum protocols. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS 2004), pp. 415–425. IEEE Computer Society (2004); Also arXiv:quant-ph/0402130 |
| [5] | Ardeshir-Larijani, E., Gay, S.J., Nagarajan, R.: Equivalence checking of quantum protocols. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 478–492. Springer, Heidelberg (2013) · Zbl 1381.68144 · doi:10.1007/978-3-642-36742-7_33 |
| [6] | Baltazar, P., Chadha, R., Mateus, P.: Quantum computation tree logic – model checking and complete calculus. International Journal of Quantum Information 6(2), 219–236 (2008) · Zbl 1151.81305 · doi:10.1142/S0219749908003530 |
| [7] | Baltazar, P., Chadha, R., Mateus, P., Sernadas, A.: Towards model-checking quantum security protocols. In: First International Conference on Quantum, Nano, and Micro Technologies, ICQNM. IEEE Computer Society (2007) · doi:10.1109/ICQNM.2007.21 |
| [8] | Bennett, C.H., Brassard, G., Crépeau, C., Jozsa, R., Peres, A., Wootters, W.K.: Teleporting an unknown quantum state via dual classical and Einstein-Podolsky-Rosen channels. Physical Review Letters 70, 1895–1899 (1993) · Zbl 1051.81505 · doi:10.1103/PhysRevLett.70.1895 |
| [9] | Canetti, R.: Universally composable security: A new paradigm for cryptographic protocols. In: 42nd IEEE Symposium on Foundations of Computer Science, FOCS, pp. 136–145. IEEE Computer Society (2001) · doi:10.1109/SFCS.2001.959888 |
| [10] | Davidson, T., Gay, S.J., Mlnařík, H., Nagarajan, R., Papanikolaou, N.: Model checking for Communicating Quantum Processes. International Journal of Unconventional Computing 8(1), 73–98 (2012) |
| [11] | Davidson, T.A.S.: Formal Verification Techniques using Quantum Process Calculus. PhD thesis, University of Warwick (2011) |
| [12] | Emerson, E.A.: Temporal and modal logic, vol. B: Formal Models and Semantics, pp. 995–1072. MIT Press (1990) · Zbl 0900.03030 |
| [13] | Feng, Y., Duan, R., Ying, M.: Bisimulation for quantum processes. In: 38th ACM Symposium on Principles of Programming Languages, POPL. ACM (2011) · Zbl 1284.68425 · doi:10.1145/1926385.1926446 |
| [14] | Feng, Y., Yu, N., Ying, M.: Model checking quantum Markov chains. arXiv:1205.2187 [quant-ph] (2012) · Zbl 1311.68086 |
| [15] | Feynman, R.P.: Simulating physics with computers. International Journal of Theoretical Physics 21(6-7), 467–488 (1982) · doi:10.1007/BF02650179 |
| [16] | Gay, S.J., Mackie, I.C. (eds.): Semantic Techniques in Quantum Computation. Cambridge University Press (2010) · Zbl 1185.68009 |
| [17] | Gay, S.J., Nagarajan, R.: Communicating quantum processes. In: 32nd ACM Symposium on Principles of Programming Languages, POPL, pp. 145–157 (2005); Also arXiv:quant-ph/0409052 · Zbl 1369.68207 |
| [18] | Gay, S.J.: Stabilizer states as a basis for density matrices. arXiv:1112.2156 (2011) |
| [19] | Gay, S.J., Nagarajan, R.: Types and typechecking for Communicating Quantum Processes. Mathematical Structures in Computer Science 16(3), 375–406 (2006) · Zbl 1122.68059 · doi:10.1017/S0960129506005263 |
| [20] | Gay, S.J., Nagarajan, R., Papanikolaou, N.: QMC: A model checker for quantum systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 543–547. Springer, Heidelberg (2008) · doi:10.1007/978-3-540-70545-1_51 |
| [21] | Gay, S.J., Papanikolaou, N., Nagarajan, R.: Specification and verification of quantum protocols. In: Semantic Techniques in Quantum Computation. Cambridge University Press (2010) · Zbl 1196.68135 |
| [22] | Gottesman, D.: Class of quantum error-correcting codes saturating the quantum Hamming bound. Physical Review A 54, 1862 (1996) · doi:10.1103/PhysRevA.54.1862 |
| [23] | Grover, L.: A fast quantum mechanical algorithm for database search. In: 28th ACM Symposium on the Theory of Computation, STOC, pp. 212–219. ACM Press (1996) · Zbl 0922.68044 · doi:10.1145/237814.237866 |
| [24] | Lalire, M.: Relations among quantum processes: bisimilarity and congruence. Mathematical Structures in Computer Science 16(3), 407–428 (2006) · Zbl 1122.68060 · doi:10.1017/S096012950600524X |
| [25] | Mateus, P., Sernadas, A.: Weakly complete axiomatization of exogenous quantum propositional logic. Information and Computation 204(5), 771–794 (2006) · Zbl 1116.03021 · doi:10.1016/j.ic.2006.02.001 |
| [26] | Mayers, D.: Unconditional Security in Quantum Cryptography. Journal of the ACM 48(3), 351–406 (2001) · Zbl 1323.94128 · doi:10.1145/382780.382781 |
| [27] | Nagarajan, R., Gay, S.J.: Formal verification of quantum protocols. arXiv:quant-ph/0203086 (March 2002) |
| [28] | Papanikolaou, N.K.: Model Checking Quantum Protocols. PhD thesis, University of Warwick (2009) |
| [29] | Selinger, P.: Towards a quantum programming language. Mathematical Structures in Computer Science 14(4), 527–586 (2004) · Zbl 1085.68014 · doi:10.1017/S0960129504004256 |
| [30] | Shor, P.W.: Algorithms for quantum computation: discrete logarithms and factoring. In: 35th IEEE Symposium on Foundations of Computer Science, FOCS (1994) · Zbl 1005.11506 · doi:10.1109/SFCS.1994.365700 |
| [31] | Trčka, N., Georgievska, S.: Branching bisimulation congruence for probabilistic systems. Electronic Notes in Theoretical Computer Science 220(3), 129–143 (2008) · Zbl 1286.68356 · doi:10.1016/j.entcs.2008.11.023 |
| [32] | Ying, M., Feng, Y., Duan, R., Ji, Z.: An algebra of quantum processes. ACM Transactions on Computational Logic 10(3), 19 (2009) · Zbl 1351.68187 · doi:10.1145/1507244.1507249 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
