Skip to main content
SpringerLink
Log in

A Coalgebraic Semantics Framework for Quantum Systems

  • Conference paper
  • First Online:
Book cover Formal Methods and Software Engineering (ICFEM 2019)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11852))

Included in the following conference series:

Abstract

As a quantum counterpart of labeled transition system (LTS), quantum labeled transition system (QLTS) is a powerful formalism for modeling quantum programs or protocols, and gives a categorical understanding for quantum computation. With the help of quantum branching monad, QLTS provides a framework extending some ideas in non-deterministic or probabilistic systems to quantum systems. In this paper, we propose the notion of reactive quantum system (RQS), a variant of QLTS, and develop a coalgebraic semantics for both QLTS and RQS by an endofunctor on the category of convex sets, which has a final coalgebra. Such a coalgebraic semantics provides a unifying abstract interpretation for both QLTS and RQS. The notions of bisimulation and simulation can be employed to compare the behavior of different types of quantum systems and judge whether a coalgebra can be behaviorally simulated by another.

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 EPUB and 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

References

  1. 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). https://doi.org/10.1007/978-3-642-36742-7_33

    Chapter  MATH  Google Scholar 

  2. Coecke, B., Kissinger, A.: Picturing Quantum Processes. Cambridge University Press, Cambridge (2017)

    Book  Google Scholar 

  3. Davidson, T.A.S.: Formal verification techniques using quantum process calculus. PhD thesis, University of Warwick, Coventry, UK (2012)

    Google Scholar 

  4. Deng, Y., Feng, Y.: Open bisimulation for quantum processes. In: Baeten, J.C.M., Ball, T., de Boer, F.S. (eds.) TCS 2012. LNCS, vol. 7604, pp. 119–133. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33475-7_9

    Chapter  Google Scholar 

  5. Feng, Y., Deng, Y., Ying, M.: Symbolic bisimulation for quantum processes. ACM Trans. Comput. Logic 15(2), 14:1–14:32 (2014)

    Article  MathSciNet  Google Scholar 

  6. Feng, Y., Duan, R., Ying, M.: Bisimulation for quantum processes. ACM Trans. Program. Lang. Syst. 34(4), 17:1–17:43 (2012)

    Article  Google Scholar 

  7. Feng, Y., Nengkun, Y., Ying, M.: Model checking quantum markov chains. J. Comput. Syst. Sci. 79(7), 1181–1198 (2013)

    Article  MathSciNet  Google Scholar 

  8. Gay, S.J., Nagarajan, R.: Communicating quantum processes. In: Proceedings of POPL 2005, pp. 145–157. ACM (2005)

    Google Scholar 

  9. Hasuo, I., Hoshino, N.: Semantics of higher-order quantum computation via geometry of interaction. Ann. Pure Appl. Logic 168(2), 404–469 (2017)

    Article  MathSciNet  Google Scholar 

  10. Hirvensalo, M.: Quantum automata theory – a review. In: Kuich, W., Rahonis, G. (eds.) Algebraic Foundations in Computer Science. LNCS, vol. 7020, pp. 146–167. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24897-9_7

    Chapter  Google Scholar 

  11. Jacobs, B.: Cambridge tracts in theoretical computer science. Introduction to Coalgebra: Towards Mathematics of States and Observation, vol. 59. Cambridge University Press, Cambridge (2016)

    MATH  Google Scholar 

  12. Kondacs, A., Watrous, J.: On the power of quantum finite state automata. In: Proceedings of FOCS 1997, pp. 66–75. IEEE Computer Society (1997)

    Google Scholar 

  13. Kubota, T., Kakutani, Y., Kato, G., Kawano, Y., Sakurada, H.: Application of a process calculus to security proofs of quantum protocols. In: Proceedings of the International Conference on Foundations of Computer Science (FCS), p. 1. The Steering Committee of The World Congress in Computer Science, Computer (2012)

    Google Scholar 

  14. Dal Lago, U., Rioli, A.: Applicative Bisimulation and Quantum \(\lambda \)-Calculi. In: Dastani, M., Sirjani, M. (eds.) FSEN 2015. LNCS, vol. 9392, pp. 54–68. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24644-4_4

    Chapter  Google Scholar 

  15. Li, L., Feng, Y.: Quantum Markov chains: description of hybrid systems, decidability of equivalence, and model checking linear-time properties. Inf. Comput. 244, 229–244 (2015)

    Article  MathSciNet  Google Scholar 

  16. Molina, A., Watrous, J.: Revisiting the simulation of quantum turing machines by quantum circuits. CoRR, abs/1808.01701 (2018)

    Google Scholar 

  17. Moore, C., Crutchfield, J.P.: Quantum automata and quantum grammars. Theor. Comput. Sci. 237(1–2), 275–306 (2000)

    Article  MathSciNet  Google Scholar 

  18. Nielsen, M.A., Chuang, I.: Quantum Computation and Quantum Information. Cambridge University Press, Cambridge (2002)

    MATH  Google Scholar 

  19. Nishimura, H., Ozawa, M.: Perfect computational equivalence between quantum turing machines and finitely generated uniform quantum circuit families. Quant. Inf. Process. 8(1), 13–24 (2009)

    Article  MathSciNet  Google Scholar 

  20. Ogawa, H.: Coalgebraic approach to equivalences of quantum systems. Master’s thesis, University of Tokyo (2014)

    Google Scholar 

  21. Roumen, F.: Coalgebraic quantum computation. In: Proceedings of QPL 2012, vol. 158, EPTCS, pp. 29–38 (2014)

    Google Scholar 

  22. Selinger, P.: Towards a quantum programming language. Math. Struct. Comput. Sci. 14(4), 527–586 (2004)

    Article  MathSciNet  Google Scholar 

  23. Sokolova, A.: Coalgebraic analysis of probabilistic systems. PhD thesis, Technische Universiteit Eindhoven (2005)

    Google Scholar 

  24. Urabe, N., Hasuo, I.: Generic forward and backward simulations III: quantitative simulations by matrices. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 451–466. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44584-6_31

    Chapter  Google Scholar 

  25. Yanofsky, N.S., Mannucci, M.: Quantum Computing for Computer Scientists. Cambridge University Press, Cambridge (2008)

    Book  Google Scholar 

  26. Ying, M.: Foundations of Quantum Programming. Morgan Kaufmann, Burlington (2016)

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  28. Ying, M., Feng, Y., Duan, R., Ji, Z.-R.: An algebra of quantum processes. ACM Trans. Comput. Logic 10(3), 191–1936 (2009)

    Article  MathSciNet  Google Scholar 

  29. Ying, S., Ying, M.: Reachability analysis of quantum Markov decision processes. Inf. Comput. 263, 31–51 (2018)

    Article  MathSciNet  Google Scholar 

Download references

Acknowledgement

We are indebted to Luis S. Barbosa and Renato Neves for helpful discussions regarding the coalgebraic framework. This work has been supported by the National Natural Science Foundation of China under grant no. 61772038, 61532019 and 61272160, and the Guangdong Science and Technology Department (Grant no.2018B010107004).

Author information

Authors and Affiliations

  1. School of Mathematical Sciences, Peking University, Beijing, China

    Ai Liu & Meng Sun

Authors
  1. Ai Liu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Meng Sun
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Meng Sun .

Editor information

Editors and Affiliations

  1. IRIT/INPT - ENSEEIHT, Toulouse, France

    Yamine Ait-Ameur

  2. Teesside University, Middlesbrough, UK

    Shengchao Qin

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Liu, A., Sun, M. (2019). A Coalgebraic Semantics Framework for Quantum Systems. In: Ait-Ameur, Y., Qin, S. (eds) Formal Methods and Software Engineering. ICFEM 2019. Lecture Notes in Computer Science(), vol 11852. Springer, Cham. https://doi.org/10.1007/978-3-030-32409-4_24

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-32409-4_24

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-32408-7

  • Online ISBN: 978-3-030-32409-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation