Measuring the constrained reachability in quantum Markov chains
- PDF / 545,888 Bytes
- 22 Pages / 439.37 x 666.142 pts Page_size
- 85 Downloads / 157 Views
Measuring the constrained reachability in quantum Markov chains Ming Xu1
· Cheng-Chao Huang2 · Yuan Feng3
Received: 22 December 2018 / Accepted: 21 October 2020 © Springer-Verlag GmbH Germany, part of Springer Nature 2020
Abstract Constrained reachability is a kind of quantitative path property, which is generally specified by multiphase until formulas originated in continuous stochastic logic. In this paper, through proposing a positive operator valued measure on the set of infinite paths, we develop an exact method to solve the constrained reachability problem for quantum Markov chains. The convergence rate of the reachability is also obtained. We then analyse the complexity of the proposed method, which turns out to be in polynomial-time w.r.t. the size of the classical state space and the dimension of the accompanied Hilbert space. Finally, our method is implemented and applied to a simple quantum protocol.
1 Introduction With the rapid development of quantum hardware, people tend to believe that special-purpose quantum computers with more than 100 qubits will be available in 5–10 years. It is conceivable that, once this becomes a reality, the development of quantum software will be crucial in harnessing the power of quantum computers. However, due to the distinguishable features of quantum mechanics, such as the no-cloning of quantum information and the nonlocal effect of entanglement, developing correct and efficient quantum programs and communication
Ming Xu was supported by the National Natural Science Foundation of China (Grant No. 11871221) and the Fundamental Research Funds for the Central Universities. Cheng-Chao Huang was supported by the Guangdong Science and Technology Department (Grant Nos. 2019A1515011689, 2018B010107004). Yuan Feng was supported by the National Key R&D Program of China (Grant No. 2018YFA0306704) and the Australian Research Council (Grant No. DP180100691).
B
Yuan Feng [email protected] Ming Xu [email protected] Cheng-Chao Huang [email protected]
1
Shanghai Key Lab of Trustworthy Computing, East China Normal University, Shanghai, China
2
Institute of Intelligent Software, Guangzhou, China
3
Centre for Quantum Software and Information, University of Technology Sydney, Sydney, Australia
123
M. Xu et al.
protocols is a challenging issue. Indeed, an attack on ID Quantique’s commercial quantum cryptographic system has already been reported [21]. Therefore, verification techniques for quantum programs and protocols are urgently needed. Formal verification methods, in particular model checking techniques, have proven effective in classical software design and system modelling [2,5]. It has proved mature as witnessed by a large number of successful industrial applications. Over the last decade, quite a few works have been done in extending model checking techniques to the verification of quantum systems [7,9–11,15,17,24,26]; we will discuss them in the related works part (Sect. 1.1). Reachability analysis plays a central role in probabilistic model checking. The
Data Loading...
