A Coalgebraic Semantics Framework for Quantum Systems

  • Ai Liu
  • Meng SunEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11852)


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.


Quantum labeled transition system Reactive quantum system Final coalgebra Bisimulation Simulation 



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).


  1. 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). Scholar
  2. 2.
    Coecke, B., Kissinger, A.: Picturing Quantum Processes. Cambridge University Press, Cambridge (2017)CrossRefGoogle Scholar
  3. 3.
    Davidson, T.A.S.: Formal verification techniques using quantum process calculus. PhD thesis, University of Warwick, Coventry, UK (2012)Google Scholar
  4. 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). Scholar
  5. 5.
    Feng, Y., Deng, Y., Ying, M.: Symbolic bisimulation for quantum processes. ACM Trans. Comput. Logic 15(2), 14:1–14:32 (2014)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Feng, Y., Duan, R., Ying, M.: Bisimulation for quantum processes. ACM Trans. Program. Lang. Syst. 34(4), 17:1–17:43 (2012)CrossRefGoogle Scholar
  7. 7.
    Feng, Y., Nengkun, Y., Ying, M.: Model checking quantum markov chains. J. Comput. Syst. Sci. 79(7), 1181–1198 (2013)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Gay, S.J., Nagarajan, R.: Communicating quantum processes. In: Proceedings of POPL 2005, pp. 145–157. ACM (2005)Google Scholar
  9. 9.
    Hasuo, I., Hoshino, N.: Semantics of higher-order quantum computation via geometry of interaction. Ann. Pure Appl. Logic 168(2), 404–469 (2017)MathSciNetCrossRefGoogle Scholar
  10. 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). Scholar
  11. 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)zbMATHGoogle Scholar
  12. 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. 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. 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). Scholar
  15. 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)MathSciNetCrossRefGoogle Scholar
  16. 16.
    Molina, A., Watrous, J.: Revisiting the simulation of quantum turing machines by quantum circuits. CoRR, abs/1808.01701 (2018)Google Scholar
  17. 17.
    Moore, C., Crutchfield, J.P.: Quantum automata and quantum grammars. Theor. Comput. Sci. 237(1–2), 275–306 (2000)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Nielsen, M.A., Chuang, I.: Quantum Computation and Quantum Information. Cambridge University Press, Cambridge (2002)zbMATHGoogle Scholar
  19. 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)MathSciNetCrossRefGoogle Scholar
  20. 20.
    Ogawa, H.: Coalgebraic approach to equivalences of quantum systems. Master’s thesis, University of Tokyo (2014)Google Scholar
  21. 21.
    Roumen, F.: Coalgebraic quantum computation. In: Proceedings of QPL 2012, vol. 158, EPTCS, pp. 29–38 (2014)Google Scholar
  22. 22.
    Selinger, P.: Towards a quantum programming language. Math. Struct. Comput. Sci. 14(4), 527–586 (2004)MathSciNetCrossRefGoogle Scholar
  23. 23.
    Sokolova, A.: Coalgebraic analysis of probabilistic systems. PhD thesis, Technische Universiteit Eindhoven (2005)Google Scholar
  24. 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). Scholar
  25. 25.
    Yanofsky, N.S., Mannucci, M.: Quantum Computing for Computer Scientists. Cambridge University Press, Cambridge (2008)CrossRefGoogle Scholar
  26. 26.
    Ying, M.: Foundations of Quantum Programming. Morgan Kaufmann, Burlington (2016)Google Scholar
  27. 27.
    Ying, M., Feng, Y.: Quantum loop programs. Acta Informatica 47(4), 221–250 (2010)MathSciNetCrossRefGoogle Scholar
  28. 28.
    Ying, M., Feng, Y., Duan, R., Ji, Z.-R.: An algebra of quantum processes. ACM Trans. Comput. Logic 10(3), 191–1936 (2009)MathSciNetCrossRefGoogle Scholar
  29. 29.
    Ying, S., Ying, M.: Reachability analysis of quantum Markov decision processes. Inf. Comput. 263, 31–51 (2018)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.School of Mathematical SciencesPeking UniversityBeijingChina

Personalised recommendations