{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,17]],"date-time":"2026-03-17T03:16:15Z","timestamp":1773717375169,"version":"3.50.1"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030452360","type":"print"},{"value":"9783030452377","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T00:00:00Z","timestamp":1587081600000},"content-version":"vor","delay-in-days":107,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>One important application of quantum process algebras is to formally verify quantum communication protocols. With a suitable notion of behavioural equivalence and a decision method, one can determine if an implementation of a protocol is consistent with its specification. Ground bisimulation is a convenient behavioural equivalence for quantum processes because of its associated coinduction proof technique. We exploit this technique to design and implement two on-the-fly algorithms for the strong and weak versions of ground bisimulation to check if two given processes in quantum CCS are equivalent. We then develop a tool that can verify interesting quantum protocols such as the BB84 quantum key distribution scheme.<\/jats:p>","DOI":"10.1007\/978-3-030-45237-7_2","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"21-38","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Verifying Quantum Communication Protocols with Ground Bisimulation"],"prefix":"10.1007","author":[{"given":"Xudong","family":"Qin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0753-418X","authenticated-orcid":false,"given":"Yuxin","family":"Deng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wenjie","family":"Du","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Aaronson, S., Gottesman, D.: Improved simulation of stabilizer circuits.Physical Review A 70(052328) (2004)","DOI":"10.1103\/PhysRevA.70.052328"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Abramsky, S., Coecke, B.: A categorical semantics of quantum protocols. In: Proceedings of the 19th IEEE Symposium on Logic in Computer Science. pp. 415\u2013425. IEEE Computer Society (2004)","DOI":"10.1109\/LICS.2004.1319636"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Ardeshir-Larijani, E., Gay, S.J., Nagarajan, R.: Automated equivalence checking of concurrent quantum systems. ACM Transactions on Computational Logic 19(4), 28:1\u201328:32 (2018)","DOI":"10.1145\/3231597"},{"issue":"1","key":"2_CR4","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1006\/jcss.1999.1683","volume":"60","author":"C Baier","year":"2000","unstructured":"Baier, C., Engelen, B., Majster-Cederbaum, M.E.: Deciding bisimilarity and similarity for probabilistic processes. Journal of Computer and System Sciences 60(1), 187\u2013231 (2000)","journal-title":"Journal of Computer and System Sciences"},{"key":"2_CR5","unstructured":"Bennett, C.H., Brassard, G.: Quantum cryptography: Public-key distribution and coin tossing. In: Proceedings of the IEEE International Conference on Computer, Systems and Signal Processing. pp. 175\u2013179 (1984)"},{"key":"2_CR6","unstructured":"Davidson, T.A.S.: Formal Verification Techniques using Quantum Process Calculus. Ph.D. thesis, University of Warwick (2011)"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Deng, Y.: Semantics of Probabilistic Processes: An Operational Approach.Springer (2015)","DOI":"10.1007\/978-3-662-45198-4"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Deng, Y., Du, W.: A local algorithm for checking probabilistic bisimilarity. In: Proceedings of the 4th International Conference on Frontier of Computer Science and Technology. pp. 401\u2013407. IEEE Computer Society (2009)","DOI":"10.1109\/FCST.2009.37"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-642-33475-7_9","volume-title":"Theoretical Computer Science","author":"Yuxin Deng","year":"2012","unstructured":"Deng, Yuxin, Feng, Yuan: Open Bisimulation for Quantum Processes. In: Baeten, Jos C.M., Ball, Tom, de Boer, Frank S. (eds.) TCS 2012. LNCS, vol. 7604, pp. 119\u2013133. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33475-7_9"},{"issue":"11","key":"2_CR10","doi-asserted-by":"publisher","first-page":"1608","DOI":"10.1016\/j.ic.2007.08.001","volume":"205","author":"Y Feng","year":"2007","unstructured":"Feng, Y., Duan, R., Ji, Z., Ying, M.: Probabilistic bisimulations for quantum processes. Information and Computation 205(11), 1608\u20131639 (2007)","journal-title":"Information and Computation"},{"issue":"2","key":"2_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2579818","volume":"15","author":"Y Feng","year":"2020","unstructured":"Feng, Y., Deng, Y., Ying, M.: Symbolic bisimulation for quantum processes. ACM Transactions on Computational Logic 15(2), 1\u201332 (2014)","journal-title":"ACM Transactions on Computational Logic"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Feng, Y., Duan, R., Ying, M.: Bisimulation for quantum processes. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 523\u2013534. ACM (2011)","DOI":"10.1145\/1925844.1926446"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-319-19249-9_17","volume-title":"FM 2015: Formal Methods","author":"Yuan Feng","year":"2015","unstructured":"Feng, Yuan, Hahn, Ernst Moritz, Turrini, Andrea, Zhang, Lijun: QPMC: A Model Checker for Quantum Programs and Protocols. In: Bj\u00f8rner, Nikolaj, de Boer, Frank (eds.) FM 2015. LNCS, vol. 9109, pp. 265\u2013272. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-19249-9_17"},{"key":"2_CR14","unstructured":"Fernandez, J.C., Mounier, L.: Verifying bisimulations \"on the fly\". In: Proceedings of the 3rd International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols. pp. 95\u2013110. North-Holland (1990)"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Gay, S.J., Nagarajan, R.: Communicating quantum processes. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 145\u2013157 (2005)","DOI":"10.1145\/1040305.1040318"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/978-3-540-70545-1_51","volume-title":"Computer Aided Verification","author":"Simon J Gay","year":"2008","unstructured":"Gay, Simon J., Nagarajan, Rajagopal, Papanikolaou, Nikolaos: QMC: A Model Checker for Quantum Systems. In: Gupta, Aarti, Malik, Sharad (eds.) CAV 2008. LNCS, vol. 5123, pp. 543\u2013547. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_51"},{"issue":"2","key":"2_CR17","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1016\/0304-3975(94)00172-F","volume":"138","author":"M Hennessy","year":"1995","unstructured":"Hennessy, M., Lin, H.: Symbolic bisimulations. Theoretical Computer Science 138(2), 353\u2013389 (1995)","journal-title":"Theoretical Computer Science"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Jorrand, P., Lalire, M.: Toward a quantum process algebra. In: Proceedings of the 1st Conference on Computing Frontiers. pp. 111\u2013119. ACM (2004)","DOI":"10.1145\/977091.977108"},{"key":"2_CR19","unstructured":"Kissinger, A.: Pictures of Processes: Automated Graph Rewriting for Monoidal Categories and Applications to Quantum Computing. Ph.D. thesis, University of Oxford (2011)"},{"key":"2_CR20","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1016\/j.jsc.2015.05.001","volume":"73","author":"T Kubota","year":"2016","unstructured":"Kubota, T., Kakutani, Y., Kato, G., Kawano, Y., Sakurada, H.: Semi-automated verification of security proofs of quantum cryptographic protocols. Journal of Symbolic Computation 73, 192\u2013220 (2016)","journal-title":"Journal of Symbolic Computation"},{"issue":"3","key":"2_CR21","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1017\/S096012950600524X","volume":"16","author":"M Lalire","year":"2006","unstructured":"Lalire, M.: Relations among quantum processes: Bisimilarity and congruence. Mathematical Structures in Computer Science 16(3), 407\u2013428 (2006)","journal-title":"Mathematical Structures in Computer Science"},{"key":"2_CR22","unstructured":"Liu, T., Li, Y., Wang, S., Ying, M., Zhan, N.: A theorem prover for quantum hoare logic and its applications. CoRR abs\/1601.03835 (2016)"},{"key":"2_CR23","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall (1989)"},{"key":"2_CR24","unstructured":"Qin, X., Deng, Y., Du, W.: QBisim (2020), https:\/\/github.com\/MartianQXD\/QBisim"},{"issue":"1","key":"2_CR25","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s002360050036","volume":"33","author":"D Sangiorgi","year":"1996","unstructured":"Sangiorgi, D.: A theory of bisimulation for the pi-calculus. Acta Informatica 33(1), 69\u201397 (1996)","journal-title":"Acta Informatica"},{"issue":"4","key":"2_CR26","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1017\/S0960129504004256","volume":"14","author":"P Selinger","year":"2004","unstructured":"Selinger, P.: Towards a quantum programming language. Mathematical Structures in Computer Science 14(4), 527\u2013586 (2004)","journal-title":"Mathematical Structures in Computer Science"},{"issue":"2","key":"2_CR27","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1103\/PhysRevLett.85.441","volume":"85","author":"P Shor","year":"2000","unstructured":"Shor, P., Preskill, J.: Simple proof of security of the BB84 quantum key distribution protocol. Physical Review Letters 85(2), 441\u2013444 (2000)","journal-title":"Physical Review Letters"},{"key":"2_CR28","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1016\/j.ic.2015.07.004","volume":"244","author":"A Turrini","year":"2015","unstructured":"Turrini, A., Hermanns, H.: Polynomial time decision algorithms for probabilistic automata. Information and Computation 244, 134\u2013171 (2015)","journal-title":"Information and Computation"},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"Ying, M., Feng, Y., Duan, R., Ji, Z.: An algebra of quantum processes. ACMTransactions on Computational Logic 10(3), 1\u201336 (2009)","DOI":"10.1145\/1507244.1507249"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Ying, M.: Foundations of Quantum Programming. Morgan Kaufmann (2016)","DOI":"10.1016\/B978-0-12-802306-8.00005-7"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45237-7_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:04:32Z","timestamp":1616436272000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45237-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030452360","9783030452377"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45237-7_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"155","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"40","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"8","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"14","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}