{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,2]],"date-time":"2026-01-02T07:49:41Z","timestamp":1767340181483,"version":"3.41.0"},"reference-count":25,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2014,4,1]],"date-time":"2014-04-01T00:00:00Z","timestamp":1396310400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"publisher","award":["DP110103473, DP130102764, and FT100100218"],"award-info":[{"award-number":["DP110103473, DP130102764, and FT100100218"]}],"id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002367","name":"Chinese Academy of Sciences","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100002367","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2014,4]]},"abstract":"<jats:p>\n            With the previous notions of bisimulation presented in the literature, to check if two quantum processes are bisimilar, we have to instantiate their free quantum variables with arbitrary quantum states, and verify the bisimilarity of the resulting configurations. This makes checking bisimilarity infeasible from an algorithmic point of view, because quantum states constitute a continuum. In this article, we introduce a\n            <jats:italic>symbolic<\/jats:italic>\n            operational semantics for quantum processes directly at the quantum operation level, which allows us to describe the bisimulation between quantum processes without resorting to quantum states. We show that the symbolic bisimulation defined here is equivalent to the open bisimulation for quantum processes in previous work, when strong bisimulations are considered. An algorithm for checking symbolic ground bisimilarity is presented. We also give a modal characterisation for quantum bisimilarity based on an extension of Hennessy-Milner logic to quantum processes.\n          <\/jats:p>","DOI":"10.1145\/2579818","type":"journal-article","created":{"date-parts":[[2014,5,7]],"date-time":"2014-05-07T12:48:53Z","timestamp":1399466933000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":23,"title":["Symbolic Bisimulation for Quantum Processes"],"prefix":"10.1145","volume":"15","author":[{"given":"Yuan","family":"Feng","sequence":"first","affiliation":[{"name":"University of Technology, Sydney, Australia, and Tsinghua University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuxin","family":"Deng","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mingsheng","family":"Ying","sequence":"additional","affiliation":[{"name":"University of Technology, Sydney, Australia, and Tsinghua University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,5,2]]},"reference":[{"volume-title":"Proceedings of the IEEE International Conference on Computer, Systems and Signal Processing. 175--179","author":"Bennett C. H.","unstructured":"C. H. Bennett and G. Brassard . 1984. Quantum cryptography: Public-key distribution and coin tossing . In Proceedings of the IEEE International Conference on Computer, Systems and Signal Processing. 175--179 . C. H. Bennett and G. Brassard. 1984. Quantum cryptography: Public-key distribution and coin tossing. In Proceedings of the IEEE International Conference on Computer, Systems and Signal Processing. 175--179.","key":"e_1_2_1_1_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_1","DOI":"10.1103\/PhysRevLett.70.1895"},{"doi-asserted-by":"publisher","key":"e_1_2_1_3_1","DOI":"10.1103\/PhysRevLett.69.2881"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.1016\/0890-5401(92)90017-A"},{"doi-asserted-by":"crossref","unstructured":"J.\n      Cheriyan T.\n      Hagerup and \n      K.\n      Mehlhorn\n  . \n  1990\n  . Can a maximum flow be computed in o(nm) time&quest; In Automata Languages and Programming M. Paterson Ed. Lecture Notes in Computer Science vol. \n  443 Springer 235--248.   J. Cheriyan T. Hagerup and K. Mehlhorn. 1990. Can a maximum flow be computed in o(nm) time&quest; In Automata Languages and Programming M. Paterson Ed. Lecture Notes in Computer Science vol. 443 Springer 235--248.","key":"e_1_2_1_5_1","DOI":"10.1007\/BFb0032035"},{"unstructured":"Y. Deng and W. Du. 2011. Logical metric and algorithmic characterisations of probabilistic bisimulation. arXiv:1103.4577v1 {cs.LO}. Tech. rep. CMU-CS-11-110 Carnegie Mellon University.  Y. Deng and W. Du. 2011. Logical metric and algorithmic characterisations of probabilistic bisimulation. arXiv:1103.4577v1 {cs.LO}. Tech. rep. CMU-CS-11-110 Carnegie Mellon University.","key":"e_1_2_1_7_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_8_1","DOI":"10.1007\/978-3-642-33475-7_9"},{"doi-asserted-by":"publisher","key":"e_1_2_1_9_1","DOI":"10.1016\/j.ic.2007.08.001"},{"doi-asserted-by":"publisher","key":"e_1_2_1_10_1","DOI":"10.1145\/1926385.1926446"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1145\/2400676.2400680"},{"doi-asserted-by":"publisher","key":"e_1_2_1_12_1","DOI":"10.1016\/j.jcss.2013.04.002"},{"volume-title":"Proceedings of the 2nd International Workshop on Developments in Computational Models.","author":"Gay S.","unstructured":"S. Gay , R. Nagarajan , and N. Papanikolaou . 2006. Probabilistic model-checking of quantum protocols . In Proceedings of the 2nd International Workshop on Developments in Computational Models. S. Gay, R. Nagarajan, and N. Papanikolaou. 2006. Probabilistic model-checking of quantum protocols. In Proceedings of the 2nd International Workshop on Developments in Computational Models.","key":"e_1_2_1_13_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_14_1","DOI":"10.1007\/978-3-540-70545-1_51"},{"doi-asserted-by":"publisher","key":"e_1_2_1_15_1","DOI":"10.1145\/1040305.1040318"},{"doi-asserted-by":"publisher","key":"e_1_2_1_16_1","DOI":"10.1006\/inco.1993.1067"},{"doi-asserted-by":"publisher","key":"e_1_2_1_17_1","DOI":"10.1016\/0304-3975(94)00172-F"},{"doi-asserted-by":"publisher","key":"e_1_2_1_18_1","DOI":"10.1145\/977091.977108"},{"volume-title":"States, Effects and Operations: Fundamental Notions of Quantum Theory","author":"Kraus K.","unstructured":"K. Kraus . 1983. States, Effects and Operations: Fundamental Notions of Quantum Theory . Springer . K. Kraus. 1983. States, Effects and Operations: Fundamental Notions of Quantum Theory. Springer.","key":"e_1_2_1_19_1"},{"volume-title":"Proceedings of the International Conference on Foundations of Computer Science (FCS'12)","author":"Kubota T.","unstructured":"T. Kubota , Y. Kakutani , G. Kato , Y. Kawano , and H. Sakurada . 2012. Application of a process calculus to security proofs of quantum protocols . In Proceedings of the International Conference on Foundations of Computer Science (FCS'12) . T. Kubota, Y. Kakutani, G. Kato, Y. Kawano, and H. Sakurada. 2012. Application of a process calculus to security proofs of quantum protocols. In Proceedings of the International Conference on Foundations of Computer Science (FCS'12).","key":"e_1_2_1_20_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_21_1","DOI":"10.1017\/S096012950600524X"},{"volume-title":"Communication and Concurrency","author":"Milner R.","unstructured":"R. Milner . 1989. Communication and Concurrency . Prentice Hall, Englewood Cliffs , NJ. R. Milner. 1989. Communication and Concurrency. Prentice Hall, Englewood Cliffs, NJ.","key":"e_1_2_1_22_1"},{"unstructured":"M. Nielsen and I. Chuang. 2000. Quantum Computation and Quantum Information. Cambridge University Press.   M. Nielsen and I. Chuang. 2000. Quantum Computation and Quantum Information. Cambridge University Press.","key":"e_1_2_1_23_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_25_1","DOI":"10.1007\/s002360050036"},{"volume-title":"States, Effects and Operations: Fundamental Notions of Quantum Theory","author":"J.","unstructured":"Neumann, J. 1955. States, Effects and Operations: Fundamental Notions of Quantum Theory . Princeton University Press . Neumann, J. 1955. States, Effects and Operations: Fundamental Notions of Quantum Theory. Princeton University Press.","key":"e_1_2_1_26_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_27_1","DOI":"10.1145\/1507244.1507249"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2579818","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2579818","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T23:43:50Z","timestamp":1750290230000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2579818"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,4]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,4]]}},"alternative-id":["10.1145\/2579818"],"URL":"https:\/\/doi.org\/10.1145\/2579818","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2014,4]]},"assertion":[{"value":"2012-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-05-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}