{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,5]],"date-time":"2026-04-05T10:20:33Z","timestamp":1775384433708,"version":"3.50.1"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2018,10,31]],"date-time":"2018-10-31T00:00:00Z","timestamp":1540944000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"School of Computer Science, Institute for Research in Fundamental Sciences"},{"name":"EU ICT COST Action IC1405 \u201cReversible Computation\u2014Extending Horizons of Computing.\u201d"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2018,10,31]]},"abstract":"<jats:p>The novel field of quantum computation and quantum information has gathered significant momentum in the last few years. It has the potential to radically impact the future of information technology and influence the development of modern society. The construction of practical, general purpose quantum computers has been challenging, but quantum cryptographic and communication devices have been available in the commercial marketplace for several years. Quantum networks have been built in various cities around the world and a dedicated satellite has been launched by China to provide secure quantum communication. Such new technologies demand rigorous analysis and verification before they can be trusted in safety- and security-critical applications. Experience with classical hardware and software systems has shown the difficulty of achieving robust and reliable implementations.<\/jats:p>\n          <jats:p>\n            We present\n            <jats:italic>\n              CCS\n              <jats:sup>q<\/jats:sup>\n            <\/jats:italic>\n            , a concurrent language for describing quantum systems, and develop verification techniques for checking equivalence between\n            <jats:italic>\n              CCS\n              <jats:sup>q<\/jats:sup>\n            <\/jats:italic>\n            processes.\n            <jats:italic>\n              CCS\n              <jats:sup>q<\/jats:sup>\n            <\/jats:italic>\n            has well-defined operational and superoperator semantics for protocols that are\n            <jats:italic>functional<\/jats:italic>\n            , in the sense of computing a deterministic input-output relation for all interleavings arising from concurrency in the system. We have implemented QEC (Quantum Equivalence Checker), a tool that takes the specification and implementation of quantum protocols, described in\n            <jats:italic>\n              CCS\n              <jats:sup>q<\/jats:sup>\n            <\/jats:italic>\n            , and automatically checks their equivalence. QEC is the first fully automatic equivalence checking tool for concurrent quantum systems. For efficiency purposes, we restrict ourselves to Clifford operators in the stabilizer formalism, but we are able to verify protocols over all input states. We have specified and verified a collection of interesting and practical quantum protocols, ranging from quantum communication and quantum cryptography to quantum error correction.\n          <\/jats:p>","DOI":"10.1145\/3231597","type":"journal-article","created":{"date-parts":[[2018,11,20]],"date-time":"2018-11-20T14:19:23Z","timestamp":1542723563000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Automated Equivalence Checking of Concurrent Quantum Systems"],"prefix":"10.1145","volume":"19","author":[{"given":"Ebrahim","family":"Ardeshir-Larijani","sequence":"first","affiliation":[{"name":"School of Computer Science, Institute for Research in Fundamental Sciences (IPM), Tehran, Iran"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simon J.","family":"Gay","sequence":"additional","affiliation":[{"name":"School of Computing Science, University of Glasgow, Glasgow, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rajagopal","family":"Nagarajan","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Faculty of Science and Technology, Middlesex University, The Burroughs, London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,11,20]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/CCC.2009.42"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.70.052328"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS\u201904)","author":"Abramsky S.","unstructured":"S. Abramsky and B. Coecke . 2004. A categorical semantics of quantum protocols . In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS\u201904) . IEEE Computer Society, 415--425. S. Abramsky and B. Coecke. 2004. A categorical semantics of quantum protocols. In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS\u201904). IEEE Computer Society, 415--425."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.73.022334"},{"key":"e_1_2_1_5_1","volume-title":"Retrieved","author":"Ardeshir-Larijani E.","year":"2013","unstructured":"E. Ardeshir-Larijani . 2013 . Quantum Equivalence Checker (QEC) . Retrieved September 10, 2018 from http:\/\/www.dcs.gla.ac.uk\/&sim;simon\/qec. E. Ardeshir-Larijani. 2013. Quantum Equivalence Checker (QEC). Retrieved September 10, 2018 from http:\/\/www.dcs.gla.ac.uk\/&sim;simon\/qec."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_33"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201914)","volume":"8413","author":"Ardeshir-Larijani E.","unstructured":"E. Ardeshir-Larijani , S. J. Gay , and R. Nagarajan . 2014. Verification of concurrent quantum protocols by equivalence checking . In Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201914) , E. \u00c1brah\u00e1m and K. Havelund (Eds.). Lecture Notes in Computer Science , Vol. 8413 . Springer, 500--514. E. Ardeshir-Larijani, S. J. Gay, and R. Nagarajan. 2014. Verification of concurrent quantum protocols by equivalence checking. In Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201914), E. \u00c1brah\u00e1m and K. Havelund (Eds.). Lecture Notes in Computer Science, Vol. 8413. Springer, 500--514."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1088\/1367-2630\/7\/1\/170"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0219749908003530"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.70.1895"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.69.2881"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1088\/1367-2630\/13\/4\/043016"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-009-9141-x"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2579818"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926446"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19249-9_17"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2013.04.002"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005378"},{"key":"e_1_2_1_21_1","volume-title":"Stabilizer states as a basis for density matrices. arXiv:1112.2156","author":"Gay S. J.","year":"2011","unstructured":"S. J. Gay . 2011. Stabilizer states as a basis for density matrices. arXiv:1112.2156 ( 2011 ). S. J. Gay. 2011. Stabilizer states as a basis for density matrices. arXiv:1112.2156 (2011)."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040318"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_51"},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"S. J. Gay R. Nagarajan and N. Papanikolaou. 2010. Specification and verification of quantum protocols. In Semantic Techniques in Quantum Computation S. J. Gay and I. C. Mackie (Eds.). Cambridge University Press.  S. J. Gay R. Nagarajan and N. Papanikolaou. 2010. Specification and verification of quantum protocols. In Semantic Techniques in Quantum Computation S. J. Gay and I. C. Mackie (Eds.). Cambridge University Press.","DOI":"10.1017\/CBO9781139193313.012"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38986-3_10"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9_22"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2920"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.59.1829"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.86.5811"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2015.05.001"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/1014989.1014992"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.77.198"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.78.042309"},{"key":"e_1_2_1_36_1","volume-title":"Retrieved","year":"2013","unstructured":"Microsoft. 2013 . Language-Integrated Quantum Operations . Retrieved September 10, 2018 from https:\/\/www.microsoft.com\/en-us\/research\/project\/language-integrated-quantum-operations-liqui. Microsoft. 2013. Language-Integrated Quantum Operations. Retrieved September 10, 2018 from https:\/\/www.microsoft.com\/en-us\/research\/project\/language-integrated-quantum-operations-liqui."},{"key":"e_1_2_1_37_1","volume-title":"Communication and Concurrency","author":"Milner R.","unstructured":"R. Milner . 1989. Communication and Concurrency . Prentice Hall , I-- XI , 1--260. R. Milner. 1989. Communication and Concurrency. Prentice Hall, I--XI, 1--260."},{"key":"e_1_2_1_38_1","volume-title":"Gay","author":"Nagarajan Rajagopal","year":"2002","unstructured":"Rajagopal Nagarajan and Simon J . Gay . 2002 . Formal verification of quantum protocols. arXiv:quant-ph\/0203086. Rajagopal Nagarajan and Simon J. Gay. 2002. Formal verification of quantum protocols. arXiv:quant-ph\/0203086."},{"key":"e_1_2_1_39_1","unstructured":"M. A. Nielsen and I. L. Chuang. 2000. Quantum Computation and Quantum Information. Cambridge University Press.   M. A. Nielsen and I. L. Chuang. 2000. Quantum Computation and Quantum Information. Cambridge University Press."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_2_1_42_1","doi-asserted-by":"crossref","unstructured":"G. F. Viamontes I. L. Markov and J. P. Hayes. 2009. Quantum Circuit Simulation. Springer I--X 1--190.   G. F. Viamontes I. L. Markov and J. P. Hayes. 2009. Quantum Circuit Simulation. Springer I--X 1--190.","DOI":"10.1007\/978-90-481-3065-8"},{"key":"e_1_2_1_43_1","doi-asserted-by":"crossref","unstructured":"Mingsheng Ying. 2016. Foundations of Quantum Programming. Morgan Kaufmann.   Mingsheng Ying. 2016. Foundations of Quantum Programming. Morgan Kaufmann.","DOI":"10.1016\/B978-0-12-802306-8.00004-5"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1507244.1507249"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.62.052316"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3231597","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3231597","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:07:03Z","timestamp":1750212423000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3231597"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10,31]]},"references-count":40,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2018,10,31]]}},"alternative-id":["10.1145\/3231597"],"URL":"https:\/\/doi.org\/10.1145\/3231597","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,10,31]]},"assertion":[{"value":"2017-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-11-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}