Document Open Access Logo

Effect Semantics for Quantum Process Calculi

Authors Lorenzo Ceragioli , Fabio Gadducci , Giuseppe Lomurno , Gabriele Tedeschi

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2024.16.pdf
  • Filesize: 0.9 MB
  • 22 pages

Document Identifiers

Author Details

Lorenzo Ceragioli
  • IMT School for Advanced Studies Lucca, Italy
Fabio Gadducci
  • University of Pisa, Italy
Giuseppe Lomurno
  • University of Pisa, Italy
Gabriele Tedeschi
  • University of Pisa, Italy

Funding

This study was carried out within the National Centre on HPC, Big Data and Quantum Computing - SPOKE 10 (Quantum Computing) and received funding from the European Union Next-GenerationEU - National Recovery and Resilience Plan (NRRP) – MISSION 4 COMPONENT 2, INVESTMENT N. 1.4 – CUP N. I53C22000690001.

Cite AsGet BibTex

Lorenzo Ceragioli, Fabio Gadducci, Giuseppe Lomurno, and Gabriele Tedeschi. Effect Semantics for Quantum Process Calculi. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 16:1-16:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CONCUR.2024.16

Abstract

The development of quantum communication protocols sparked the interest in quantum extensions of process calculi and behavioural equivalences, but defining a bisimilarity that matches the observational properties of a quantum-capable system is a surprisingly difficult task. The two proposals explicitly addressing this issue, qCCS and lqCCS, do not define an algorithmic verification scheme: the bisimilarity of two processes is proven by comparing their behaviour under all input states. We introduce a new semantic model based on effects, i.e. probabilistic predicates on quantum states that represent their observable properties. We define and investigate the properties of effect distributions and effect labelled transition systems (eLTSs), generalizing probability distributions and probabilistic labelled transition systems (pLTSs), respectively. As a proof of concept, we provide an eLTS-based semantics for a minimal quantum process algebra, which we prove sound and complete with respect to the observable probabilistic behaviour of quantum processes. To the best of our knowledge, ours is the first algorithmically verifiable proposal that abides to the properties of quantum theory.

Subject Classification

ACM Subject Classification
  • Theory of computation → Quantum computation theory
  • Theory of computation → Process calculi
  • Theory of computation → Operational semantics
Keywords
  • Quantum process calculi
  • probabilistic LTSs
  • effect LTSs

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Samson Abramsky, Rui Soares Barbosa, Nadish de Silva, and Octavio Zapata. The quantum monad on relational structures. In Kim G. Larsen, Hans L. Bodlaender, and Jean-François Raskin, editors, MFCS 2017, volume 83 of LIPIcs, pages 35:1-35:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPICS.MFCS.2017.35.
  2. Charles H. Bennett and Gilles Brassard. Quantum cryptography: Public key distribution and coin tossing. Theoretical Computer Science, 560:7-11, 2014. URL: https://doi.org/10.1016/j.tcs.2014.05.025.
  3. Charles H. Bennett, Gilles Brassard, Claude Crépeau, Richard Jozsa, Asher Peres, and William K. Wootters. Teleporting an unknown quantum state via dual classical and Einstein-Podolsky-Rosen channels. Physical Review Letters, 70:1895-1899, 1993. URL: https://doi.org/10.1103/PhysRevLett.70.1895.
  4. Filippo Bonchi, Alexandra Silva, and Ana Sokolova. The power of convex algebras. In Roland Meyer, Uwe Nestmann, and Marc Herbstritt, editors, CONCUR 2017, volume 85 of LIPIcs, pages 23:1-23:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPICS.CONCUR.2017.23.
  5. Marcello Caleffi, Angela Sara Cacciapuoti, and Giuseppe Bianchi. Quantum internet: from communication to distributed computing! In Jón Atli Benediktsson and Falko Dressler, editors, NANOCOM 2018, pages 3:1-3:4. ACM, 2018. URL: https://doi.org/10.1145/3233188.3233224.
  6. Lorenzo Ceragioli, Fabio Gadducci, Giuseppe Lomurno, and Gabriele Tedeschi. Quantum bisimilarity via barbs and contexts: Curbing the power of non-deterministic observers (extended version). CoRR, abs/2311.06116, 2023. URL: https://doi.org/10.48550/arXiv.2311.06116.
  7. Lorenzo Ceragioli, Fabio Gadducci, Giuseppe Lomurno, and Gabriele Tedeschi. Quantum bisimilarity via barbs and contexts: Curbing the power of non-deterministic observers. Proceedings of the ACM on Programming Languages, 8(POPL):43:1269-43:1297, 2024. URL: https://doi.org/10.1145/3632885.
  8. Timothy A. S. Davidson. Formal Verification Techniques Using Quantum Process Calculus. PhD thesis, University of Warwick, 2012. Google Scholar
  9. Yuxin Deng. Bisimulations for probabilistic and quantum processes. In Sven Schewe and Lijun Zhang, editors, CONCUR 2018, volume 118 of LIPIcs, pages 2:1-2:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.2.
  10. Yuxin Deng and Yuan Feng. Open bisimulation for quantum processes. In Jos C. M. Baeten, Thomas Ball, and Frank S. de Boer, editors, TCS 2012, volume 7604 of LNCS, pages 119-133. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-33475-7_9.
  11. Yuan Feng, Yuxin Deng, and Mingsheng Ying. Symbolic bisimulation for quantum processes. ACM Transactions on Computational Logic, 15(2):14:1-14:32, 2014. URL: https://doi.org/10.1145/2579818.
  12. Yuan Feng, Runyao Duan, and Mingsheng Ying. Bisimulation for quantum processes. ACM Transactions on Programming Languages and Systems, 34(4):17:1-17:43, 2012. URL: https://doi.org/10.1145/2400676.2400680.
  13. Yuan Feng and Mingsheng Ying. Toward automatic verification of quantum cryptographic protocols. In Luca Aceto and David de Frutos-Escrig, editors, CONCUR 2015, volume 42 of LIPIcs, pages 441-455. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2015.441.
  14. Fei Gao, SuJuan Qin, Wei Huang, and QiaoYan Wen. Quantum private query: A new kind of practical quantum cryptographic protocol. Science China Physics, Mechanics & Astronomy, 62(7):70301, 2019. URL: https://doi.org/10.1007/s11433-018-9324-6.
  15. Simon J. Gay and Rajagopal Nagarajan. Communicating quantum processes. In Jens Palsberg and Martín Abadi, editors, POPL 2005, pages 145-157. ACM, 2005. URL: https://doi.org/10.1145/1040305.1040318.
  16. Stanley Gudder. Quantum Markov chains. Journal of Mathematical Physics, 49(7):072105, 2008. URL: https://doi.org/10.1063/1.2953952.
  17. Ichiro Hasuo and Naohiko Hoshino. Semantics of higher-order quantum computation via geometry of interaction. In LICS 2011, pages 237-246. IEEE Computer Society, 2011. URL: https://doi.org/10.1109/LICS.2011.26.
  18. Teiko Heinosaari and Mário Ziman. The Mathematical Language of Quantum Theory: From Uncertainty to Entanglement. Cambridge University Press, 2011. Google Scholar
  19. Matthew Hennessy. Exploring probabilistic bisimulations, part I. Formal Aspects of Computing, 24(4-6):749-768, 2012. URL: https://doi.org/10.1007/s00165-012-0242-7.
  20. Matthew Hennessy and Huimin Lin. Symbolic bisimulations. Theoretical Computer Science, 138(2):353-389, 1995. URL: https://doi.org/10.1016/0304-3975(94)00172-F.
  21. Bart Jacobs. Probabilities, distribution monads, and convex categories. Theoretical Computer Science, 412(28):3323-3336, June 2011. URL: https://doi.org/10.1016/j.tcs.2011.04.005.
  22. Jules Jacobs and Thorsten Wißmann. Fast coalgebraic bisimilarity minimization. Proceedings of the ACM on Programming Languages, 7(POPL):52:1514-52:1541, 2023. URL: https://doi.org/10.1145/3571245.
  23. Takahiro Kubota, Yoshihiko Kakutani, Go Kato, Yasuhito Kawano, and Hideki Sakurada. Application of a process calculus to security proofs of quantum protocols. In Hamid R. Arabnia, George A. Gravvanis, and Ashu M. G. Solo, editors, FCS 2012, pages 141-147. CSREA Press, 2012. Google Scholar
  24. Marie Lalire. Relations among quantum processes: Bisimilarity and congruence. Mathematical Structures in Computer Science, 16(3):407-428, 2006. URL: https://doi.org/10.1017/S096012950600524X.
  25. Marie Lalire and Philippe Jorrand. A process algebraic approach to concurrent and distributed quantum computation: Operational semantics. CoRR, quant-ph/0407005, 2004. URL: https://arxiv.org/abs/quant-ph/0407005.
  26. Kim G. Larsen and Arne Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1-28, 1991. URL: https://doi.org/10.1016/0890-5401(91)90030-6.
  27. Ai Liu and Meng Sun. A coalgebraic semantics framework for quantum systems. In Yamine Aït Ameur and Shengchao Qin, editors, ICFEM 2019, volume 11852 of LNCS, pages 387-402. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-32409-4_24.
  28. Gui-lu Long, Fu-guo Deng, Chuan Wang, Xi-Han Li, Kai Wen, and Wan-Ying Wang. Quantum secure direct communication and deterministic secure quantum communication. Frontiers of Physics in China, 2(3):251-272, 2007. URL: https://doi.org/10.1007/s11467-007-0050-3.
  29. Dominic Mayers. Unconditional security in quantum cryptography. Journal of the ACM, 48(3):351-406, 2001. URL: https://doi.org/10.1145/382780.382781.
  30. Michael A. Nielsen and Isaac L. Chuang. Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press, 2010. Google Scholar
  31. Ali Ibnun Nurhadi and Nana Rachmana Syambas. Quantum key distribution (QKD) protocols: A survey. In ICWT 2018, pages 1-5. IEEE, 2018. URL: https://doi.org/10.1109/ICWT.2018.8527822.
  32. Hiroshi Ogawa. Coalgebraic approach to equivalences of quantum systems. Master’s thesis, University of Tokyo, 2014. Google Scholar
  33. Sam Staton. Relating coalgebraic notions of bisimulation. Logical Methods in Computer Science, 7(1), 2011. URL: https://doi.org/10.2168/LMCS-7(1:13)2011.
  34. Yong Wang. Probabilistic process algebra to unifying quantum and classical computing in closed systems. International Journal of Theoretical Physics, 58(10):3436-3509, 2019. URL: https://doi.org/10.1007/s10773-019-04216-2.
  35. Peiying Zhang, Ning Chen, Shigen Shen, Shui Yu, Sheng Wu, and Neeraj Kumar. Future quantum communications and networking: A review and vision. IEEE Wireless Communications, 31(1):141-148, 2024. URL: https://doi.org/10.1109/MWC.012.2200295.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact