(Un)decidable Problems about Reachability of Quantum Systems

  • Yangjia Li
  • Mingsheng Ying
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8704)


We study the reachability problem of a quantum system modeled by a quantum automaton, namely, a set of processes each of which is formalized as a quantum unitary transformation. The reachable sets are chosen to be boolean combinations of (closed) subspaces of the state Hilbert space of the quantum system. Four different reachability properties are considered: eventually reachable, globally reachable, ultimately forever reachable, and infinitely often reachable. The main result of this paper is that all of the four reachability properties are undecidable in general; however, the last three become decidable if the reachable sets are boolean combinations without negation.


Quantum reachability verification Skolem’s problem 2-counter Minsky machine undecidability 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Altafini, C., Ticozzi, F.: Modeling and control of quantum systems: An introduction. IEEE Transactions on Automatic Control 57, 1898 (2012)CrossRefMathSciNetGoogle Scholar
  2. 2.
    Amano, M., Iwama, K.: Undecidability on quantum finite automata. In: Proceedings of the Thirty-First Annual ACM Symposium on Theory of Computing (STOC), pp. 368–375 (1999)Google Scholar
  3. 3.
    Ardeshir-Larijani, E., Gay, S.J., Nagarajan, R.: Equivalence checking of quantum protocols. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 478–492. Springer, Heidelberg (2013)Google Scholar
  4. 4.
    Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)Google Scholar
  5. 5.
    Berstel, J., Mignotte, M.: Deux propriétés décidables des suites récurrentes linéaires. Bull. Soc. Math. France 104, 175–184 (1976)Google Scholar
  6. 6.
    Birkhoff, G., von Neumann, J.: The Logic of Quantum Mechanics. Annals of Mathematics 37, 823–843 (1936)Google Scholar
  7. 7.
    Blondel, V.D., Jeandel, E., Koiran, P., Portier, N.: Decidable and undecidable problems about quantum automata. SIAM Journal on Computing 34, 1464–1473 (2005)Google Scholar
  8. 8.
    Cassaigne, J., Karhumäki, J.: Examples of undecidable problems for 2-generator matrix semigroups. Theoretical Computer Science 204, 29–34 (1998)Google Scholar
  9. 9.
    Cirac, J.I., Zoller, P.: Goals and opportunities in quantum simulation. Nature Physics 8, 264–266 (2012)Google Scholar
  10. 10.
    Eisert, J., Müller, M.P., Gogolin, C.: Quantum measurement occurrence is undecidable. Physcal Review Letters 108, 260501 (2012)Google Scholar
  11. 11.
    Gay, S.J., Nagarajan, R., Papanikolaou, N.: Specification and verification of quantum protocols. In: Gay, S.J., Mackie, I. (eds.) Semantic Techniques in Quantum Computation, pp. 414–472. Cambridge University Press (2010)Google Scholar
  12. 12.
    Green, A.S., Lumsdaine, P.L., Ross, N.J., Selinger, P., Valiron, B.: Quipper: A scalable quantum programming language. In: Proceedings of the 34th ACM Conference on Programming Language Design and Implementation (PLDI), pp. 333–342 (2013)Google Scholar
  13. 13.
    Halava, V., Harju, T., Hirvensalo, M., Karhumäki, J.: Skolem’s Problem: On the Border between Decidability and Undecidability, Technical Report 683, Turku Centre for Computer Science (2005)Google Scholar
  14. 14.
    Kondacs, A., Watrous, J.: On the power of quantum finite state automata. In: Proc. 38th Symposium on Foundation of Computer Science (FOCS), pp. 66–75 (1997)Google Scholar
  15. 15.
    Lech, C.: A note on recurring series. Ark. Mat. 2, 417–421 (1953)Google Scholar
  16. 16.
    Li, Y.J., Yu, N.K., Ying, M.S.: Termination of nondeterministic quantum programs. Acta Informatica 51, 1–24 (2014)Google Scholar
  17. 17.
    Mahler, K.: Eine arithmetische eigenschaft der Taylor koeffizienten rationaler funktionen. In: Proc. Akad. Wet. Amsterdam, vol. 38 (1935)Google Scholar
  18. 18.
    Minsky, M.L.: Computation: finite and infinite machines. Prentice-Hall (1967)Google Scholar
  19. 19.
    Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information. Cambridge University Press (2000)Google Scholar
  20. 20.
    Paz, A.: Introduction to probabilistic automata. Academic Press, New York (1971)Google Scholar
  21. 21.
    Post, E.L.: A variant of a recursively unsolvable problem. Bulletin of the American Mathematical Society 52, 264–268 (1946)Google Scholar
  22. 22.
    Ouaknine, J., Worrell, J.: Decision Problems for Linear Recurrence Sequences. In: Finkel, A., Leroux, J., Potapov, I. (eds.) RP 2012. LNCS, vol. 7550, pp. 21–28. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  23. 23.
    Salomaa, A., Soittola, M.: Automata-Theoretic Aspects of Formal Power Series. Springer (1978)Google Scholar
  24. 24.
    Skolem, T.: Ein verfahren zur behandlung gewisser exponentialer gleichungen. In: Proceedings of the 8th Congress of Scandinavian Mathematicians, Stockholm, pp. 163–188 (1934)Google Scholar
  25. 25.
    Schirmer, S.G., Solomon, A.I., Leahy, J.V.: Criteria for reachability of quantum states. Journal of Physics A: Mathematical and General 35, 8551–8562 (2002)Google Scholar
  26. 26.
    Ying, M.S.: Floyd-Hoare logic for quantum programs. ACM Transactions on Programming Languages and Systems (19) (2011)Google Scholar
  27. 27.
    Ying, M.S., Yu, N.K., Feng, Y., Duan, R.Y.: Verification of quantum programs. Science of Computer Programming 78, 1679–1700 (2013)Google Scholar
  28. 28.
    Ying, S., Feng, Y., Yu, N., Ying, M.: Reachability probabilities of quantum Markov chains. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 334–348. Springer, Heidelberg (2013)Google Scholar
  29. 29.
    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)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Yangjia Li
    • 1
  • Mingsheng Ying
    • 2
  1. 1.Tsinghua UniversityChina
  2. 2.University of TechnologySydneyAustralia

Personalised recommendations