{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:35:03Z","timestamp":1781238903224,"version":"3.54.1"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2012,12,1]],"date-time":"2012-12-01T00:00:00Z","timestamp":1354320000000},"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":["DP110103473DP130102764FT100100218"],"award-info":[{"award-number":["DP110103473DP130102764FT100100218"]}],"id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2012,12]]},"abstract":"<jats:p>Quantum cryptographic systems have been commercially available, with a striking advantage over classical systems that their security and ability to detect the presence of eavesdropping are provable based on the principles of quantum mechanics. On the other hand, quantum protocol designers may commit more faults than classical protocol designers since human intuition is poorly adapted to the quantum world. To offer formal techniques for modeling and verification of quantum protocols, several quantum extensions of process algebra have been proposed. An important issue in quantum process algebra is to discover a quantum generalization of bisimulation preserved by various process constructs, in particular, parallel composition, where one of the major differences between classical and quantum systems, namely quantum entanglement, is present. Quite a few versions of bisimulation have been defined for quantum processes in the literature, but in the best case they are only proved to be preserved by parallel composition of purely quantum processes where no classical communication is involved.<\/jats:p>\n          <jats:p>Many quantum cryptographic protocols, however, employ the LOCC (Local Operations and Classical Communication) scheme, where classical communication must be explicitly specified. So, a notion of bisimulation preserved by parallel composition in the circumstance of both classical and quantum communication is crucial for process algebra approach to verification of quantum cryptographic protocols. In this article we introduce novel notions of strong bisimulation and weak bisimulation for quantum processes, and prove that they are congruent with respect to various process algebra combinators including parallel composition even when both classical and quantum communication are present. We also establish some basic algebraic laws for these bisimulations. In particular, we show the uniqueness of the solutions to recursive equations of quantum processes, which proves useful in verifying complex quantum protocols. To capture the idea that a quantum process approximately implements its specification, and provide techniques and tools for approximate reasoning, a quantified version of strong bisimulation, which defines for each pair of quantum processes a bisimulation-based distance characterizing the extent to which they are strongly bisimilar, is also introduced.<\/jats:p>","DOI":"10.1145\/2400676.2400680","type":"journal-article","created":{"date-parts":[[2013,1,11]],"date-time":"2013-01-11T15:42:48Z","timestamp":1357918968000},"page":"1-43","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":26,"title":["Bisimulation for Quantum Processes"],"prefix":"10.1145","volume":"34","author":[{"given":"Yuan","family":"Feng","sequence":"first","affiliation":[{"name":"University of Technology, Sydney, Australia, and Tsinghua University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Runyao","family":"Duan","sequence":"additional","affiliation":[{"name":"University of Technology, Sydney, Australia, and Tsinghua University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mingsheng","family":"Ying","sequence":"additional","affiliation":[{"name":"University of Technology, Sydney, Australia, and Tsinghua University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2012,12]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/266420.266432"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/647766.736021"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129599002984"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.69.2881"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.70.1895"},{"key":"e_1_2_1_6_1","unstructured":"Deng Y. and Du W. 2011. Logical metric and algorithmic characterisations of probabilistic bisimulation. arxiv:1103.4577v1 {cs.lo}. Deng Y. and Du W. 2011. Logical metric and algorithmic characterisations of probabilistic bisimulation. arxiv:1103.4577v1 {cs.lo}."},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Deng Y. Palamidessi C. and Pang J. 2005. Compositional reasoning for probabilistic finite-state behaviors. In Processes Terms and Cycles: Steps on the Road to Infinity. 309--337. Deng Y. Palamidessi C. and Pang J. 2005. Compositional reasoning for probabilistic finite-state behaviors. In Processes Terms and Cycles: Steps on the Road to Infinity . 309--337.","DOI":"10.1007\/11601548_17"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.10.033"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.013"},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the International Conference on Concurrency Theory (CONCUR). 355--370","author":"Desharnais J.","unstructured":"Desharnais , J. , Gupta , V. , Jagadeesan , R. , and Panangaden , P . 2002. Weak bisimulation is sound and complete for PCTL* . In Proceedings of the International Conference on Concurrency Theory (CONCUR). 355--370 . Desharnais, J., Gupta, V., Jagadeesan, R., and Panangaden, P. 2002. Weak bisimulation is sound and complete for PCTL*. In Proceedings of the International Conference on Concurrency Theory (CONCUR). 355--370."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.09.013"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2009.11.002"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.08.001"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926446"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040318"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the IFIP WG 2.2\/2.3 Working Conference on Programming Concepts and Methods. North-Holland","author":"Giacalone A.","unstructured":"Giacalone , A. , Jou , C. , and Smolka , S . 1990. Algebraic reasoning for probabilistic concurrent systems . In Proceedings of the IFIP WG 2.2\/2.3 Working Conference on Programming Concepts and Methods. North-Holland , Amsterdam, 443--458. Giacalone, A., Jou, C., and Smolka, S. 1990. Algebraic reasoning for probabilistic concurrent systems. In Proceedings of the IFIP WG 2.2\/2.3 Working Conference on Programming Concepts and Methods. North-Holland, Amsterdam, 443--458."},{"key":"e_1_2_1_17_1","first-page":"2","article-title":"Quantum mechanics helps in searching for a needle in a haystack","volume":"78","author":"Grover L. K.","year":"1997","unstructured":"Grover , L. K. 1997 . Quantum mechanics helps in searching for a needle in a haystack . Phys. Rev. Lett. 78 , 2 , 325. Grover, L. K. 1997. Quantum mechanics helps in searching for a needle in a haystack. Phys. Rev. Lett. 78, 2, 325.","journal-title":"Phys. Rev. Lett."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01642508"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1067"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/977091.977108"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1070\/RM1997v052n06ABEH002155"},{"key":"e_1_2_1_22_1","volume-title":"States, Effects and Operations: Fundamental Notions of Quantum Theory","author":"Kraus K.","unstructured":"Kraus , K. 1983. States, Effects and Operations: Fundamental Notions of Quantum Theory . Springer , Berlin . Kraus, K. 1983. States, Effects and Operations: Fundamental Notions of Quantum Theory. Springer, Berlin."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950600524X"},{"key":"e_1_2_1_24_1","volume-title":"Communication and Concurrency","author":"Milner R.","unstructured":"Milner , R. 1989. Communication and Concurrency . Prentice Hall , Englewood Cliffs, NJ . Milner, R. 1989. Communication and Concurrency. Prentice Hall, Englewood Cliffs, NJ."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"e_1_2_1_26_1","unstructured":"Nielsen M. and Chuang I. 2000. Quantum Computation and Quantum Information. Cambridge University Press. Nielsen M. and Chuang I. 2000. Quantum Computation and Quantum Information . Cambridge University Press."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1994.365700"},{"key":"e_1_2_1_28_1","unstructured":"van Breugel F. 2010. http:\/\/www.sti.uniurb.it\/events\/sfm10qapl\/slides\/franck-part1.pdf. van Breugel F. 2010. http:\/\/www.sti.uniurb.it\/events\/sfm10qapl\/slides\/franck-part1.pdf."},{"key":"e_1_2_1_29_1","volume-title":"Mathematical Foundations of Quantum Mechanics","author":"von Neumann J.","unstructured":"von Neumann , J. 1955. Mathematical Foundations of Quantum Mechanics . Princeton University Press , Princeton, NJ . von Neumann, J. 1955. Mathematical Foundations of Quantum Mechanics. Princeton University Press, Princeton, NJ."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1507244.1507249"},{"key":"e_1_2_1_31_1","volume-title":"Topology in Process Calculus: Approximate Correctness and Infinite Evolution of Concurrent Programs","author":"Ying M. S.","unstructured":"Ying , M. S. 2001. Topology in Process Calculus: Approximate Correctness and Infinite Evolution of Concurrent Programs . Springer New York . Ying, M. S. 2001. Topology in Process Calculus: Approximate Correctness and Infinite Evolution of Concurrent Programs. Springer New York."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00124-4"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2400676.2400680","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2400676.2400680","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:35:01Z","timestamp":1750239301000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2400676.2400680"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,12]]},"references-count":32,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2012,12]]}},"alternative-id":["10.1145\/2400676.2400680"],"URL":"https:\/\/doi.org\/10.1145\/2400676.2400680","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,12]]},"assertion":[{"value":"2011-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-12-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}