Abstract
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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Altafini, C., Ticozzi, F.: Modeling and control of quantum systems: An introduction. IEEE Transactions on Automatic Control 57, 1898 (2012)
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)
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)
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)
Berstel, J., Mignotte, M.: Deux propriétés décidables des suites récurrentes linéaires. Bull. Soc. Math. France 104, 175–184 (1976)
Birkhoff, G., von Neumann, J.: The Logic of Quantum Mechanics. Annals of Mathematics 37, 823–843 (1936)
Blondel, V.D., Jeandel, E., Koiran, P., Portier, N.: Decidable and undecidable problems about quantum automata. SIAM Journal on Computing 34, 1464–1473 (2005)
Cassaigne, J., Karhumäki, J.: Examples of undecidable problems for 2-generator matrix semigroups. Theoretical Computer Science 204, 29–34 (1998)
Cirac, J.I., Zoller, P.: Goals and opportunities in quantum simulation. Nature Physics 8, 264–266 (2012)
Eisert, J., Müller, M.P., Gogolin, C.: Quantum measurement occurrence is undecidable. Physcal Review Letters 108, 260501 (2012)
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)
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)
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)
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)
Lech, C.: A note on recurring series. Ark. Mat. 2, 417–421 (1953)
Li, Y.J., Yu, N.K., Ying, M.S.: Termination of nondeterministic quantum programs. Acta Informatica 51, 1–24 (2014)
Mahler, K.: Eine arithmetische eigenschaft der Taylor koeffizienten rationaler funktionen. In: Proc. Akad. Wet. Amsterdam, vol. 38 (1935)
Minsky, M.L.: Computation: finite and infinite machines. Prentice-Hall (1967)
Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information. Cambridge University Press (2000)
Paz, A.: Introduction to probabilistic automata. Academic Press, New York (1971)
Post, E.L.: A variant of a recursively unsolvable problem. Bulletin of the American Mathematical Society 52, 264–268 (1946)
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)
Salomaa, A., Soittola, M.: Automata-Theoretic Aspects of Formal Power Series. Springer (1978)
Skolem, T.: Ein verfahren zur behandlung gewisser exponentialer gleichungen. In: Proceedings of the 8th Congress of Scandinavian Mathematicians, Stockholm, pp. 163–188 (1934)
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)
Ying, M.S.: Floyd-Hoare logic for quantum programs. ACM Transactions on Programming Languages and Systems (19) (2011)
Ying, M.S., Yu, N.K., Feng, Y., Duan, R.Y.: Verification of quantum programs. Science of Computer Programming 78, 1679–1700 (2013)
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)
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
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Li, Y., Ying, M. (2014). (Un)decidable Problems about Reachability of Quantum Systems. In: Baldan, P., Gorla, D. (eds) CONCUR 2014 – Concurrency Theory. CONCUR 2014. Lecture Notes in Computer Science, vol 8704. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44584-6_33
Download citation
DOI: https://doi.org/10.1007/978-3-662-44584-6_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-44583-9
Online ISBN: 978-3-662-44584-6
eBook Packages: Computer ScienceComputer Science (R0)