PLQP & Company: Decidable Logics for Quantum Algorithms
Tóm tắt
We introduce a probabilistic modal (dynamic-epistemic) quantum logic PLQP for reasoning about quantum algorithms. We illustrate its expressivity by using it to encode the correctness of the well-known quantum search algorithm, as well as of a quantum protocol known to solve one of the paradigmatic tasks from classical distributed computing (the leader election problem). We also provide a general method (extending an idea employed in the decidability proof in Dunn et al. (J. Symb. Log. 70:353–359, 2005)) for proving the decidability of a range of quantum logics, interpreted on finite-dimensional Hilbert spaces. We give general conditions for the applicability of this method, and in particular we apply it to prove the decidability of PLQP.
Tài liệu tham khảo
Baltag, A., Smets, S.: LQP: the dynamic logic of quantum information. Math. Struct. Comput. Sci. 16, 491–525 (2006)
Baltag, A., Smets, S.: A dynamic—logical perspective on quantum behavior. In: Douven, I., Horsten, L. (eds.) Studia Logica, vol. 89, pp. 185–209 (2008), special issue on Applied Logic in the Philosophy of Science
Baltag, A., Smets, S.: Correlated knowledge: an epistemic-logic view on quantum entanglement. Int. J. Theor. Phys. 49, 3005–3021 (2010)
Baltag, A., Smets, S.: Quantum logic as a dynamic logic. Synthese 179, 285–306 (2011). T. Kuipers, J. van Benthem, and H. Visser (eds.)
Baltag, A., Smets, S.: Correlated information: a logic for multi-partite quantum systems. Electron. Notes Theor. Comput. Sci. 27, 3–14 (2011). B. Coecke and P. Panangaden (eds.)
Baltag, A., Smets, S.: The dynamic turn in quantum logic. Synthese 186, 753–773 (2012)
Birkhoff, G., von Neumann, J.: The logic of quantum mechanics. Ann. Math. 37, 823–843 (1936)
Blackburn, P., van Benthem, J.: Modal logic: a semantic perspective. In: Blackburn, P., van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logic, pp. 1–84. Elsevier, Amsterdam (2007)
Caviness, B.F., Johnson, J.R. (eds.): Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer, New York (1998)
Collins, G.E.: Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) Automata Theory and Formal Languages 2nd GI Conference, Kaiserslautern, 20–23 May 1975, pp. 134–183. Springer, Berlin (1975)
Dalla Chiara, M., Giuntini, R., Greechie, R.: Reasoning in Quantum Theory, Sharp and Unsharp Quantum Logics. Kluwer Academic, Dordrecht (2004)
Dunn, J.M., Hagge, T.J., Moss, L.S., Wang, Z.: Quantum logic as motivated by quantum computing. J. Symb. Log. 70, 353–359 (2005)
Engesser, K., Gabbay, D.M., Lehmann, D. (eds.): Handbook of Quantum Logic and Quantum Structures. Elsevier, Amsterdam (2007)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)
Fine, K.: Propositional quantifiers in modal logic. Theoria 36, 336–346 (1970)
Grover, L.: Quantum mechanics helps in searching for a needle in a haystack. Phys. Rev. Lett. 79, 325–328 (1997)
Harel, H., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)
Hennessy, M., Milner, R.: On observing nondeterminism and concurrency. In: de Bakker, J., van Leeuwen, J. (eds.) Automata, Languages and Programming, pp. 299–309. Springer, Berlin (1980)
Hintikka, J.: Knowledge and Belief: An Introduction to the Logic of the Two Notions. Cornell University Press, Cornell (1962)
D’Hondt, E.: Distributed quantum computation: a measurement-based approach. Ph.D. Thesis, Vrije Universiteit Brussel (2005)
D’Hondt, E., Panangaden, P.: The computational power of the W and GHZ states. Quantum Inf. Comput. 6, 173–183 (2006)
Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information. Cambridge University Press, Cambridge (2010)
Tarski, A.: A Decision Method for Elementary Algebra and Geometry. RAND Corporation, Santa Monica (1948)