Skip to main content
SpringerLink
Log in

Reachability and Termination Analysis of Concurrent Quantum Programs

  • Conference paper
CONCUR 2012 – Concurrency Theory (CONCUR 2012)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7454))

Included in the following conference series:

Abstract

We introduce a Markov chain model of concurrent quantum programs. This model is a quantum generalization of Hart, Sharir and Pnueli’s probabilistic concurrent programs. Some characterizations of the reachable space, uniformly repeatedly reachable space and termination of a concurrent quantum program are derived by the analysis of their mathematical structures. Based on these characterizations, algorithms for computing the reachable space and uniformly repeatedly reachable space and for deciding the termination are given.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Cirac, J.I., Ekert, A.K., Huelga, S.F., Macchiavello, C.: Distributed quantum computation over noisy channels. Physical Review A 59, 4249–4254 (1999)

    Article  MathSciNet  Google Scholar 

  2. Don, C., Shmuel, W.: Matrix multiplication via arithmetic progressions. Journal of Symbolic Computation 9, 251–280 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  3. Davidson, T.A.S.: Formal Verification Techniques using Quantum Process Calculus, Ph.D. thesis. University of Warwick (2011)

    Google Scholar 

  4. Davidson, T.A.S., Gay, S., Nagarajan, R., Puthoor, I.V.: Analysis of a quantum error correcting code using quantum process calculus. In: Proceedingds of QPL 2011, the 8th Workhop on Quantum Physics and Logic, pp. 107–120 (2011)

    Google Scholar 

  5. D’Hondt, E., Panangaden, P.: Quantum weakest preconditions. Mathematical Structures in Computer Science 16, 429–451 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  6. Feng, Y., Duan, R.Y., Ji, Z.F., Ying, M.S.: Probabilistic bisimulations for quantum processes. Information and Computation 205, 1608–1639 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  7. Feng, Y., Duan, R.Y., Ying, M.S.: Bisimulation for quantum processes. In: Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 523–534 (2011)

    Google Scholar 

  8. Gay, S.J., Nagarajan, R.: Communicating Quantum Processes. In: Proceedings of the 32nd ACM Symposium on Principles of Programming Languages (POPL), pp. 145–157 (2005)

    Google Scholar 

  9. Gay, S.J., Nagarajan, R.: Types and typechecking for communicating quantum processes. Mathematical Structures in Computer Science 16, 375–406 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  10. Gay, S.J., Nagarajan, R., Papanikolaou, N.: QMC: A Model Checker for Quantum Systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 543–547. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  11. Gay, S.J., Papanikolaou, N., Nagarajan, R.: 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. Hart, S., Sharir, M., Pnueli, A.: Termination of probabilistic concurrent programs. ACM Transactions on Programming Languages and Systems 5, 356–380 (1983)

    Article  MATH  Google Scholar 

  13. Jorrand, P., Lalire, M.: Toward a quantum process algebra. In: Proceedings of the First ACM Conference on Computing Frontiers, pp. 111–119 (2004)

    Google Scholar 

  14. Lalire, M.: Relations among quantum processes: bisimilarity and congruence. Mathematical Structures in Computer Science 16, 407–428 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  15. Lalire, M., Jorrand, P.: A process algebraic approach to concurrent and distributed quantum computation: operational semantics. In: Proceedings of the 2nd International Workshop on Quantum Programming Languages (2004)

    Google Scholar 

  16. Li, Y.Y., Yu, N.K., Ying, M.S.: Termination of nondeterministic quantum programs. Short presentation of LICS (2012), (For full paper, see arXiv: 1201.0891)

    Google Scholar 

  17. Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information. Cambridge University Press, Cambridge (2000)

    MATH  Google Scholar 

  18. Selinger, P.: Towards a quantum programming language. Mathematical Structure in Computer Science 14, 527–586 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  19. Sharir, M., Pnueli, A., Hart, S.: Verification of probabilistic programs. SIAM Journal on Computing 13, 292–314 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  20. Ying, M.S.: Floyd-Hoare logic for quantum programs. ACM Transactions on Programming Languages and Systems 33, art. no: 19 (2011)

    Google Scholar 

  21. Ying, M.S., Feng, Y.: An algebraic language for distributed quantum computing. IEEE Transactions on Computers 58, 728–743 (2009)

    Article  MathSciNet  Google Scholar 

  22. Ying, M.S., Feng, Y., Duan, R.Y., Ji, Z.F.: An algebra of quantum processes. ACM Transactions on Computational Logic 10, art. no. 19 (2009)

    Google Scholar 

  23. Ying, M.S., Feng, Y.: Quantum loop programs. Acta Informatica 47, 221–250 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  24. Ying, M.S., Yu, N.K., Feng, Y., Duan, R.Y.: Verification of Quantum Programs, arXiv:1106.4063

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Tsinghua University, China

    Nengkun Yu

  2. University of Technology, Sydney, Australia

    Mingsheng Ying

Authors
  1. Nengkun Yu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mingsheng Ying
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing Science, Newcastle University, Claremont Tower, Claremont Road, NE1 7RU, Newcastle upon Tyne, UK

    Maciej Koutny

  2. Department of Computer Science, University of Leicester, Computer Science Building, University Road, LE1 7RH, Leicester, UK

    Irek Ulidowski

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Yu, N., Ying, M. (2012). Reachability and Termination Analysis of Concurrent Quantum Programs. In: Koutny, M., Ulidowski, I. (eds) CONCUR 2012 – Concurrency Theory. CONCUR 2012. Lecture Notes in Computer Science, vol 7454. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32940-1_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-32940-1_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-32939-5

  • Online ISBN: 978-3-642-32940-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation