zbMATH — the first resource for mathematics

Model checking quantum Markov chains. (English) Zbl 1311.68086
Summary: Although security of quantum cryptography is provable based on principles of quantum mechanics, it can be compromised by flaws in the design of quantum protocols. So, it is indispensable to develop techniques for verifying and debugging quantum cryptographic systems. Model-checking has proved to be effective in the verification of classical cryptographic protocols, but an essential difficulty arises when it is applied to quantum systems: the state space of a quantum system is always a continuum even when its dimension is finite. To overcome this difficulty, we introduce a novel notion of quantum Markov chain, especially suited for modelling quantum cryptographic protocols, in which quantum effects are encoded as super-operators labelling transitions, leaving the location information (nodes) being classical. Then we define a quantum extension of probabilistic computation tree logic (PCTL) and develop a model-checking algorithm for quantum Markov chains.

68Q60 Specification and verification (program logics, model checking, etc.)
81P94 Quantum cryptography (quantum-theoretic aspects)
81S25 Quantum stochastic calculus
94A60 Cryptography
Full Text: DOI
[1] Accardi, L., Nonrelativistic quantum mechanics as a noncommutative Markov process, Adv. Math., 20, 329, (1976) · Zbl 0367.60119
[2] Baier, C.; Katoen, J. P., Principles of model checking, (2008), MIT Press
[3] Baltazar, P.; Chadha, R.; Mateus, P., Quantum computation tree logic - model checking and complete calculus, Int. J. Quantum Inform., 6, 219-236, (2008) · Zbl 1151.81305
[4] Bennett, C. H.; Brassard, G., Quantum cryptography: public-key distribution and coin tossing, (Proceedings of the IEEE International Conference on Computer, Systems and Signal Processing, (1984)), 175-179
[5] Bennett, C. H.; Brassard, G.; Crepeau, C.; Jozsa, R.; Peres, A.; Wootters, W., Teleporting an unknown quantum state via dual classical and EPR channels, Phys. Rev. Lett., 70, 1895-1899, (1993) · Zbl 1051.81505
[6] Bennett, C. H.; Wiesner, S. J., Communication via one- and two-particle operators on Einstein-Podolsky-Rosen states, Phys. Rev. Lett., 69, 20, 2881-2884, (1992) · Zbl 0968.81506
[7] Billingsley, P., Probability and measure, (2008), Wiley-India
[8] Breuer, H. P.; Petruccione, F., The theory of open quantum systems, (2002), Oxford University Press Oxford
[9] Clarke, E. M.; Grumberg, O.; Peled, D., Model checking, (1999), MIT Press
[10] Diestel, J.; Uhl, J. J., Vector measures, (1977), Amer. Math. Soc. · Zbl 0369.46039
[11] Emerson, E., Temporal and modal logic, (Handbook of Theoretical Computer Science, vol. 2, (1990)), 995-1072 · Zbl 0900.03030
[12] Faigle, U.; Schönhuth, A., Discrete quantum Markov chains, (2010)
[13] Gay, S.; Nagarajan, R.; Papanikolaou, N., Probabilistic model-checking of quantum protocols, (Proceedings of the 2nd International Workshop on Developments in Computational Models, (2006))
[14] Gay, S.; Nagarajan, R.; Papanikolaou, N., QMC: A model checker for quantum systems, (CAV ʼ08, (2008), Springer), 543-547
[15] Gudder, S., Quantum Markov chains, J. Math. Phys., 49, 7, 072105, (2008) · Zbl 1152.81457
[16] Hansson, H.; Jonsson, B., A logic for reasoning about time and reliability, Formal Aspects Comput., 6, 5, 512-535, (September 1994)
[17] Horn, R. A.; Johnson, C. R., Matrix analysis, (1990), Cambridge University Press · Zbl 0704.15002
[18] Hung, W. N.N.; Song, X.; Yang, G.; Yang, J.; Perkowski, M., Quantum logic synthesis by symbolic reachability analysis, (Proceedings of the 41st Design Automation Conference, (July 2004)), 838-841
[19] Hung, W. N.N.; Song, X.; Yang, G.; Yang, J.; Perkowski, M., Optimal synthesis of multiple output Boolean functions using a set of quantum gates by symbolic reachability analysis, IEEE Trans. Comput. Aided Design Integrated Circuits Syst., 25, 9, 1652-1663, (2006)
[20] Kraus, K., States, effects and operations: fundamental notions of quantum theory, (1983), Springer Berlin
[21] Kwiatkowska, M.; Norman, G.; Parker, D., Stochastic model checking, (Formal Methods for Performance Evaluation, (2007)), 220-270 · Zbl 1323.68379
[22] Lowe, G., Breaking and fixing the needham-schroeder public-key protocol using FDR, (Tools and Algorithms for the Construction and Analysis of Systems, (1996)), 147-166
[23] von Neumann, J., Mathematical foundations of quantum mechanics, (1955), Princeton University Press Princeton, NJ
[24] Nielsen, M.; Chuang, I., Quantum computation and quantum information, (2000), Cambridge University Press · Zbl 1049.81015
[25] Papanikolaou, N. K., Model checking quantum protocols, (2008), PhD thesis
[26] NEC: · Zbl 0266.20038
[27] Selinger, P., Towards a quantum programming language, Math. Structures Comput. Sci., 14, 4, 527-586, (2004) · Zbl 1085.68014
[28] Tani, S.; Kobayashi, H.; Matsumoto, K., Exact quantum algorithms for the leader election problem, ACM Trans. Comput. Theory, 4, 1, (March 2012)
[29] Vardi, M. Y., Automatic verification of probabilistic concurrent finite state programs, (Proceedings of the 26th IEEE FOCS, (1985)), 327-338
[30] Ying, M. S.; Yu, N. K.; Feng, Y.; Duan, R. Y., Verification of quantum programs, (2011), Manuscript. Available online at:
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.