Abstract
We introduce the notion of recursive quantum Markov chain (RQMC) for analysing recursive quantum programs with procedure calls. RQMCs are natural extension of Etessami and Yannakakis’s recursive Markov chains where the probabilities along transitions are replaced by completely positive and trace-nonincreasing super-operators on a state Hilbert space of a quantum system.
We study the reachability problem for RQMCs and establish a reduction from it to computing the least solution of a system of polynomial equations in the semiring of super-operators. It is shown that for an important subclass of RQMCs, namely linear RQMCs, the reachability problem can be solved in polynomial time. For general case, technique of Newtonian program analysis recently developed by Esparza, Kiefer and Luttenberger is employed to approximate reachability super-operators. A polynomial time algorithm that computes the support subspaces of the reachability super-operators in general case is also proposed.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Accardi, L.: Nonrelativistic quantum mechanics as a noncommutative Markov process. Advances in Mathematics 20(3), 329–366 (1976)
Alur, R., Benedikt, M., Etessami, K., Godefroid, P., Reps, T., Yannakakis, M.: Analysis of recursive state machines. ACM Transactions on Programming Languages and Systems 27(4), 786–818 (2005)
Alur, R., Etessami, K., Yannakakis, M.: Analysis of recursive state machines. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 207–220. Springer, Heidelberg (2001)
Bennett, C.H., Brassard, G., Crepeau, C., Jozsa, R., Peres, A., Wootters, W.: Teleporting an unknown quantum state via dual classical and EPR channels. Physical Review Letters 70, 1895–1899 (1993)
Bennett, C.H., Wiesner, S.J.: Communication via one- and two-particle operators on Einstein-Podolsky-Rosen states. Physical Review Letters 69(20), 2881–2884 (1992)
Breuer, H., Petruccione, F.: The theory of open quantum systems. Oxford University Press, New York (2002)
Esparza, J., Kiefer, S., Luttenberger, M.: Newtonian program analysis. Journal of the ACMÂ 57(6), 33 (2010)
Esparza, J., Kucera, A., Mayr, R.: Model checking probabilistic pushdown automata. In: IEEE Symposium on Logic in Computer Science (LICS 2004), pp. 12–21 (July 2004)
Etessami, K., Yannakakis, M.: Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations. Journal of the ACMÂ 56(1), 1 (2009)
Faigle, U., Schönhuth, A.: Discrete Quantum Markov Chains. Arxiv.org/abs/1011.1295 (2010)
Feng, Y., Yu, N., Ying, M.: Model checking quantum Markov chains. Journal of Computer and System Sciences 79, 1181–1198 (2013)
Gudder, S.: Quantum Markov chains. Journal of Mathematical Physics 49(7), 072105, 14 (2008)
Kraus, K.: States, Effects and Operations: Fundamental Notions of Quantum Theory. Springer, Berlin (1983)
von Neumann, J.: Mathematical Foundations of Quantum Mechanics. Princeton University Press, Princeton (1955)
Nielsen, M., Chuang, I.: Quantum computation and quantum information. Cambridge University Press (2000)
Selinger, P.: Towards a quantum programming language. Mathematical Structures in Computer Science 14(4), 527–586 (2004)
Steel, A.: A new algorithm for the computation of canonical forms of matrices over fields. Journal of Symbolic Computation 24(3-4), 409–432 (1997)
Watrous, J.: Lecture Notes on Theory of Quantum Information (2011), https://cs.uwaterloo.ca/~watrous/CS766/
Ying, M., Li, Y., Yu, N., Feng, Y.: Model-Checking Linear-Time Properties of Quantum Systems. Arxiv.org/abs/1101.0303. Submitted to ACM Transactions on Computational Logic (revised)
Ying, M., Yu, N., Feng, Y., Duan, R.: Verification of Quantum Programs. Science of Computer Programming 78, 1679–1700 (2013)
Yu, N., Ying, M.: Reachability and Termination Analysis of Concurrent Quantum Programs. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 69–83. Springer, Heidelberg (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Feng, Y., Yu, N., Ying, M. (2013). Reachability Analysis of Recursive Quantum Markov Chains. In: Chatterjee, K., Sgall, J. (eds) Mathematical Foundations of Computer Science 2013. MFCS 2013. Lecture Notes in Computer Science, vol 8087. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40313-2_35
Download citation
DOI: https://doi.org/10.1007/978-3-642-40313-2_35
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40312-5
Online ISBN: 978-3-642-40313-2
eBook Packages: Computer ScienceComputer Science (R0)