A Logic for Quantum Circuits and Protocols

  • Manas Patra
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3722)


A logic for reasoning about quantum circuits and protocols is proposed. It incorporates the basic features of quantum theory-probability, unitary dynamics, tensor products and measurement. The underlying language could be used for verification and synthesis of quantum circuits. Important algorithms like the quantum search algorithm of Grover are discussed. The logic also forms the foundation on which more elaborate formal systems for reasoning about quantum protocols could be based. A sound and complete axiomatization is presented. Algorithms for circuit verification, circuit equivalence (exact and approximate) are outlined. Some related complexity issues are also discussed.


Probability logic quantum computing quantum circuits complexity 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [AC04]
    Abramsky, S., Coecke, B.: A categorical semantics of quantum protocols. Research Report RR-04-02, Oxford University Computing Laboratory (2004)Google Scholar
  2. [BKR86]
    Ben-Or, M., Kozen, D., Reif, J.H.: The complexity of elementary algebra and geometry. Journal of Computer and System Sciences 32(1), 251–264 (1986)zbMATHCrossRefMathSciNetGoogle Scholar
  3. [BPR03]
    Basu, S., Pollack, R., Roy, M.-F.: Algorithms in real algebraic geometry. Springer, Heidelberg (2003)zbMATHGoogle Scholar
  4. [BS04]
    Baltag, A., Smets, S.: A logic for quantum programs. In: Proc. of QPL 2004, pp. 39–56 (2004)Google Scholar
  5. [BV97]
    Bernstein, E., Vazirani, U.V.: Quantum complexity theory. SIAM. J. Computing 26(5), 1411–1473 (1997)zbMATHCrossRefMathSciNetGoogle Scholar
  6. [Can88]
    Canny, J.F.: Some algebraic and geometric computations in PSPACE. In: Proc. 20th ACM Symp. on Theory of Computing, pp. 460–467 (1988)Google Scholar
  7. [CGL05]
    Dalla Chiara, M.L., Guntini, R., Leporoni, R.: Quantum computational logics and fock space semantics. Int. Journal of quantum information 3(1), 9–16 (2005)zbMATHCrossRefGoogle Scholar
  8. [FHM90]
    Fagin, R., Halpern, J.Y., Megiddo, N.: A logic for reasoning about probabilities. Information and Computation 87(1/2), 78–128 (1990)zbMATHCrossRefMathSciNetGoogle Scholar
  9. [Gro96]
    Grover, L.: A fast quantum mechanical algorithm for database search. In: Proc. 28th. annual ACM symposium on Theory of computing, pp. 210–212. ACM, New York (1996)Google Scholar
  10. [Imm89]
    Immerman, N.: Descriptive and computational complexity. In: Computational complexity theory. In: Proc. Symp. App. Math., pp. 75–91. AMS (1989)Google Scholar
  11. [MP03a]
    van der Meyden, R., Patra, M.: Knowledge in quantum systems. In: Theoretical aspects of knowledge and rationality. ACM, Bloomington (2003)Google Scholar
  12. [MP03b]
    van der Meyden, R., Patra, M.: A logic for probability in quantum systems. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol. 2803, pp. 427–440. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  13. [MS04]
    Mateus, P., Serandas, A.: Reasoning about quantum systems. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol. 3229, pp. 239–251. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  14. [NC01]
    Nielsen, M.A., Chuang, I.L.: Quantum computation and information. CUP (2001)Google Scholar
  15. [Nie03]
    Nielsen, M.: Universal quantum computation using only projective measurement, quantum memory, and preparation of the 0 state. Physics Lett. A 308(2-3), 96–100 (2003)zbMATHCrossRefGoogle Scholar
  16. [Pat04]
    Patra, M.: Logics for quantum computation and information, (2004)
  17. [PBL95]
    Grabowski, M., Busch, P., Lathi, P.J.: Operational Quantum Physics. Springer, Berlin (1995)zbMATHGoogle Scholar
  18. [RPFS65]
    Leighton, R.B., Feynman, R.P., Sands, M.: Feynman Lectures on Physics, vol. III. Addison-Wesely, Reading (1965)zbMATHGoogle Scholar
  19. [Sho67]
    Shoenfield, J.R.: Mathematical Logic. Addison-Wesley, Reading (1967)zbMATHGoogle Scholar
  20. [Smu61]
    Smullyan, R.M.: Theory of Formal Systems. Princeton University Press, Princeton (1961)zbMATHGoogle Scholar
  21. [vT03]
    van Tonder, A.: A lambda calculus for quantum computation. arXiv e-Print (2003),
  22. [Yao93]
    Yao, A.C.-C.: Quantum circuit complexity. In: Proc. 34th. Symp. on Foundations of computer science, pp. 352–360. IEEE, Los Alamitos (1993)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Manas Patra
    • 1
    • 2
  1. 1.School of Computer Science and EngineeringThe University of New South WalesSydneyAustralia
  2. 2.CQCTMacquarie UniversitySydneyAustralia

Personalised recommendations