{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T16:54:59Z","timestamp":1781283299328,"version":"3.54.1"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"6","funder":[{"name":"JAIST Research Grant for Fundamental Research"},{"name":"JST SICORP","award":["JPMJSC20C2"],"award-info":[{"award-number":["JPMJSC20C2"]}]},{"name":"JSPS KAKENHI","award":["JP23K28060, JP23K19959, JP24K20757, JP24KK0185, and JP24K23858"],"award-info":[{"award-number":["JP23K28060, JP23K19959, JP24K20757, JP24KK0185, and JP24K23858"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2025,7,31]]},"abstract":"<jats:p>While constructing practical quantum computers by big companies remains a challenge, the application of quantum communication and cryptography has made remarkable progress. Therefore, it is crucial to verify quantum protocols before they can be trusted in safety and security-critical applications. We have proposed Basic Dynamic Quantum Logic (BDQL) to formalize and verify sequential models of quantum protocols with a support tool developed in Maude. However, BDQL does not support concurrency in its formalization. This article introduces Concurrent Dynamic Quantum Logic (CDQL), an extension of BDQL, to formalize and verify concurrent models of quantum protocols. CDQL is more expressive than BDQL by considering concurrent behavior and communication among participants in quantum protocols. Since CDQL is a conservative extension of BDQL, we extend the syntax of BDQL to CDQL and make a transformation from CDQL to BDQL without interrupting the semantics of BDQL. We also extend the implementation of BDQL to support CDQL, making a new support tool in Maude. The new support tool is equipped with a lazy rewriting strategy to make the verification process significantly faster. Several quantum communication protocols are successfully formalized and verified in BDQL\/CDQL, demonstrating the effectiveness of our automated approach and tool in verifying quantum protocols.<\/jats:p>","DOI":"10.1145\/3708475","type":"journal-article","created":{"date-parts":[[2024,12,12]],"date-time":"2024-12-12T16:57:34Z","timestamp":1734022654000},"page":"1-36","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Automated Quantum Protocol Verification Based on Concurrent Dynamic Quantum Logic"],"prefix":"10.1145","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1601-4584","authenticated-orcid":false,"given":"Canh Minh","family":"Do","sequence":"first","affiliation":[{"name":"Computing Science, Japan Advanced Institute of Science and Technology, Nomi, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9890-1015","authenticated-orcid":false,"given":"Tsubasa","family":"Takagi","sequence":"additional","affiliation":[{"name":"Computing Science, Japan Advanced Institute of Science and Technology, Nomi, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4441-3259","authenticated-orcid":false,"given":"Kazuhiro","family":"Ogata","sequence":"additional","affiliation":[{"name":"Computing Science, Japan Advanced Institute of Science and Technology, Nomi, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,7,3]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_42"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","unstructured":"Ebrahim Ardeshir-Larijani Simon J. Gay and Rajagopal Nagarajan. 2018. Automated equivalence checking of concurrent quantum systems. ACM Transactions on Computational Logic 19 4 Article 28 (Nov. 2018) 32 pages. DOI: 10.1145\/3231597","DOI":"10.1145\/3231597"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","unstructured":"A. Baltag and S. Smets. 2006. LQP: The dynamic logic of quantum information. Mathematical Structures in Computer Science 16 3 (2006) 491\u2013525. DOI: 10.1017\/S0960129506005299","DOI":"10.1017\/S0960129506005299"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","unstructured":"Charles H. Bennett Gilles Brassard Claude Cr\u00e9peau Richard Jozsa Asher Peres and William K. Wootters. 1993. Teleporting an unknown quantum state via dual classical and Einstein-Podolsky-Rosen channels. Physical Review Letters 70 13 (1993) 1895\u20131899. DOI: 10.1103\/PhysRevLett.70.1895","DOI":"10.1103\/PhysRevLett.70.1895"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1038\/nature23474"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","unstructured":"G. Birkhoff and J. von Neumann. 1936. The logic of quantum mechanics. Annals of Mathematics 57 4 (1936) 823\u2013843. DOI: 10.2307\/1968621","DOI":"10.2307\/1968621"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","unstructured":"Yu-Ao Chen Qiang Zhang Teng-Yun Chen Wenqi Cai Shengkai Liao Jun Zhang Kai Chen Juan Yin Ji-Gang Ren Zhu Chen et al. 2021. An integrated space-to-ground quantum communication network over 4 600 kilometres. Nature 589 (2021) 214\u2013219. DOI: 10.1038\/s41586-020-03093-8","DOI":"10.1038\/s41586-020-03093-8"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","unstructured":"Sheng-Tzong Cheng Chun-Yen Wang and Ming-Hon Tao. 2005. Quantum communication for wireless wide-area networks. IEEE Journal on Selected Areas in Communications 23 7 (2005) 1424\u20131432. DOI: 10.1109\/JSAC.2005.851157","DOI":"10.1109\/JSAC.2005.851157"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71999-1"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33475-7_9"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100021162"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.18293\/SEKE2023-014"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","unstructured":"Canh Minh Do and Kazuhiro Ogata. 2024. Symbolic model checking quantum circuits in Maude. PeerJ Computer Science 10 (2024) e2098. DOI: 10.7717\/PEERJ-CS.2098","DOI":"10.7717\/PEERJ-CS.2098"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","unstructured":"Artur K. Ekert. 1991. Quantum cryptography based on Bell\u2019s theorem. Physical Review Letters 67 6 (Aug. 1991) 661\u2013663. DOI: 10.1103\/PhysRevLett.67.661","DOI":"10.1103\/PhysRevLett.67.661"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","unstructured":"Mohamed Elboukhari Mostafa Azizi and Abdelmalek Azizi. 2010. Verification of quantum cryptography protocols by model checking. International Journal of Network Security & Its Applications 2 (Oct. 2010). DOI: 10.5121\/ijnsa.2010.2404","DOI":"10.5121\/ijnsa.2010.2404"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","unstructured":"Chip Elliott. 2004. The DARPA quantum network. arXiv.quant-ph\/0412029. Retrieved from 10.48550\/arXiv.quant-ph\/0412029","DOI":"10.48550\/arXiv.quant-ph\/0412029"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1126\/science.1057726"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","unstructured":"Yuan Feng Sanjiang Li and Mingsheng Ying. 2022. Verification of distributed quantum programs. ACM Transactions on Computational Logic 23 3 Article 19 (Apr. 2022) 40 pages. DOI: 10.1145\/3517145","DOI":"10.1145\/3517145"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","unstructured":"Wan Fokkink. 2000. Introduction to Process Algebra. Springer. DOI: 10.1007\/978-3-662-04293-9","DOI":"10.1007\/978-3-662-04293-9"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","unstructured":"Simon Gay and Rajagopal Nagarajan. 2004. Communicating quantum processes. arXiv:quant-ph\/0409052. DOI: 10.1145\/1040305.1040318","DOI":"10.1145\/1040305.1040318"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","unstructured":"Simon Gay Rajagopal Nagarajan and Nikolaos Papanikolaou. 2005. Probabilistic model\u2013checking of quantum protocols. arXiv:quant-ph\/0504007. Retrieved from 10.48550\/ARXIV.QUANT-PH\/0504007","DOI":"10.48550\/ARXIV.QUANT-PH\/0504007"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1038\/46503"},{"key":"e_1_3_1_24_2","first-page":"175","volume-title":"Proceedings of the International Conference on Computer System and Signal Processing","author":"H Bennett C.","year":"1984","unstructured":"Bennett C. H. 1984. Quantum cryptography: Public key distribution and coin tossing. In Proceedings of the International Conference on Computer System and Signal Processing. IEEE, 175\u2013179. Retrieved from https:\/\/cir.nii.ac.jp\/crid\/1573950399056246784"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","unstructured":"Gary M. Hardegree. 1974. The conditional in quantum logic. Synthese (1974) 63\u201380. DOI: 10.1007\/978-94-010-9466-5_4","DOI":"10.1007\/978-94-010-9466-5_4"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-0456-4_2"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.103.150502"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","unstructured":"Shima Hassanpour and Monireh Houshmand. 2014. Bidirectional quantum teleportation and secure direct communication via entanglement swapping. arXiv:1411.0206. Retrieved from 10.48550\/arXiv.1411.0206","DOI":"10.48550\/arXiv.1411.0206"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","unstructured":"L. Herman E. L. Marsden and R. Piziak. 1975. Implication connectives in orthomodular lattices. Notre Dame Journal of Formal Logic 16 3 (1975) 305\u2013328. DOI: 10.1305\/ndjfl\/1093891789","DOI":"10.1305\/ndjfl\/1093891789"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","unstructured":"Mark Hillery Vladim\u00edr Bu\u017eek and Andr\u00e9 Berthiaume. 1999. Quantum secret sharing. Physical Review A 59 3 (1999) 1829\u20131834. DOI: 10.1103\/PhysRevA.59.1829","DOI":"10.1103\/PhysRevA.59.1829"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","unstructured":"M. \u017bukowski A. Zeilinger M. A. Horne and A. K. Ekert. 1993. \u201cEvent-ready-detectors\u201d Bell experiment via entanglement swapping. Physical Review Letters 71 26 (1993) 4287\u20134290. DOI: 10.1103\/PhysRevLett.71.4287","DOI":"10.1103\/PhysRevLett.71.4287"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","unstructured":"Sheng-Kai Liao Wen-Qi Cai Wei-Yue Liu Liang Zhang Yang Li Ji-Gang Ren Juan Yin Qi Shen Yuan Cao Zheng-Ping Li et al. 2017. Satellite-to-ground quantum key distribution. Nature 549 7670 (Aug. 2017) 43\u201347. DOI: 10.1038\/nature23655","DOI":"10.1038\/nature23655"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.69.052303"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.06.003"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","unstructured":"Rajagopal Nagarajan and Simon Gay. 2002. Formal verification of quantum protocols. arXiv:quant-ph\/0203086. Retrieved from 10.48550\/ARXIV.QUANT-PH\/0203086","DOI":"10.48550\/ARXIV.QUANT-PH\/0203086"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","unstructured":"Michael A. Nielsen and Isaac L. Chuang. 2011. Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press. DOI: 10.1017\/CBO9780511976667","DOI":"10.1017\/CBO9780511976667"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","unstructured":"Rhea Parekh Andrea Ricciardi Ahmed Darwish and Stephen DiAdamo. 2021. Quantum algorithms and simulation for parallel and distributed quantum computing. In Proceedings of the 2021 IEEE\/ACM 2nd International Workshop on Quantum Computing Software (QCS \u201921) 9\u201319. DOI: 10.1109\/QCS54837.2021.00005","DOI":"10.1109\/QCS54837.2021.00005"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1364\/OFC.2009.OThL2"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45237-7_2"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-015-9026-6"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","unstructured":"Gustavo Rigolin. 2005. Quantum teleportation of an arbitrary two-qubit state and its relation to multipartite entanglement. Physical Review A 71 3 (Mar. 2005) 032303. DOI: 10.1103\/PhysRevA.71.032303","DOI":"10.1103\/PhysRevA.71.032303"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","unstructured":"M. Sasaki M. Fujiwra H. Ishizuka W. Klaus K. Wakui M. Takeoka A. Tanaka K. Yoshino Y. Nambu S. Takahashi et al. 2011. Tokyo QKD network and the evolution to secure photonic network. In Laser Science to Photonic Applications (CLEO 2011) 1\u20133. DOI: 10.1364\/CLEO_AT.2011.JTuC1","DOI":"10.1364\/CLEO_AT.2011.JTuC1"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","unstructured":"Wenjun Shi Qinxiang Cao Yuxin Deng Hanru Jiang and Yuan Feng. 2021. Symbolic reasoning about quantum circuits in Coq. Journal of Computer Science and Technology 36 6 (2021) 1291\u20131306. DOI: 10.1007\/s11390-021-1637-9","DOI":"10.1007\/s11390-021-1637-9"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1994.365700"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-51777-8_5"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","unstructured":"Zebo Yang Maede Zolanvari and Raj Jain. 2023. A survey of important issues in quantum computing and communications. IEEE Communications Surveys & Tutorials 25 2 (2023) 1059\u20131094. DOI: 10.1109\/COMST.2023.3254481","DOI":"10.1109\/COMST.2023.3254481"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","unstructured":"Mingsheng Ying. 2012. Floyd\u2013Hoare logic for quantum programs. ACM Transactions on Programming Languages and Systems 33 6 (2012) 1\u201349. DOI: 10.1145\/2049706.2049708","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1016\/C2014-0-02660-3"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","unstructured":"Mingsheng Ying Yuan Feng Runyao Duan and Zhengfeng Ji. 2009. An algebra of quantum processes. ACM Transactions on Computational Logic 10 3 Article 19 (Apr. 2009) 36 pages. DOI: 10.1145\/1507244.1507249","DOI":"10.1145\/1507244.1507249"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3708475","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T06:37:48Z","timestamp":1751611068000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3708475"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,7,3]]},"references-count":49,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2025,7,31]]}},"alternative-id":["10.1145\/3708475"],"URL":"https:\/\/doi.org\/10.1145\/3708475","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,7,3]]},"assertion":[{"value":"2023-12-27","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-26","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-07-03","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}