{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T16:02:21Z","timestamp":1781193741456,"version":"3.54.1"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032280787","type":"print"},{"value":"9783032280794","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-28079-4_2","type":"book-chapter","created":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:32:44Z","timestamp":1781191964000},"page":"25-47","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["DisQ: A Model of\u00a0Distributed Quantum Processors"],"prefix":"10.1007","author":[{"given":"Le","family":"Chang","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Saitej","family":"Yavvari","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rance","family":"Cleaveland","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Samik","family":"Basu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Runzhou","family":"Tao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Liyi","family":"Li","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,6,12]]},"reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-642-36742-7_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Ardeshir-Larijani","year":"2013","unstructured":"Ardeshir-Larijani, E., Gay, S.J., Nagarajan, R.: Equivalence checking of quantum protocols. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 478\u2013492. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_33"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/978-3-642-54862-8_42","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Ardeshir-Larijani","year":"2014","unstructured":"Ardeshir-Larijani, E., Gay, S.J., Nagarajan, R.: Verification of concurrent quantum protocols by equivalence checking. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 500\u2013514. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_42"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/3-540-45635-X_19","volume-title":"Logic Programming","author":"S Basu","year":"2001","unstructured":"Basu, S., Mukund, M., Ramakrishnan, C.R., Ramakrishnan, I.V., Verma, R.: Local and symbolic bisimulation using tabled constraint logic programming. In: Codognet, P. (ed.) ICLP 2001. LNCS, vol. 2237, pp. 166\u2013180. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45635-X_19"},{"key":"2_CR4","doi-asserted-by":"publisher","unstructured":"Bennett, C.H., Brassard, G., Cr\u00e9peau, C., Jozsa, R., Peres, A., Wootters, W.K.: Teleporting an unknown quantum state via dual classical and einstein-podolsky-rosen channels. Phys. Rev. Lett. 70, 1895\u20131899 (1993). https:\/\/doi.org\/10.1103\/PhysRevLett.70.1895. https:\/\/link.aps.org\/doi\/10.1103\/PhysRevLett.70.1895","DOI":"10.1103\/PhysRevLett.70.1895"},{"key":"2_CR5","doi-asserted-by":"publisher","unstructured":"Berry, G., Boudol, G.: The chemical abstract machine. Theor. Comput. Sci. 96(1), 217\u2013248 (1992). https:\/\/doi.org\/10.1016\/0304-3975(92)90185-I. https:\/\/www.sciencedirect.com\/science\/article\/pii\/030439759290185I","DOI":"10.1016\/0304-3975(92)90185-I"},{"key":"2_CR6","unstructured":"Caleffi, M., et al.: Distributed quantum computing: a Survey (2022)"},{"key":"2_CR7","unstructured":"Chang, L., Yavvari, S., Cleaveland, R., Basu, S., Tao, R., Li, L.: Disq: a model of distributed quantum processors (2025). https:\/\/arxiv.org\/abs\/2407.09710"},{"key":"2_CR8","doi-asserted-by":"publisher","unstructured":"Chen, W., et al.: Scalable and programmable phononic network with trapped ions. Nat. Phys. 19(6), 877\u2013883 (2023). https:\/\/doi.org\/10.1038\/s41567-023-01952-5","DOI":"10.1038\/s41567-023-01952-5"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Chu, C., F, et al.: Titan: a distributed large-scale trapped-ion nisq computer (2024). https:\/\/arxiv.org\/abs\/2402.11021","DOI":"10.1145\/3649329.3655908"},{"key":"2_CR10","doi-asserted-by":"publisher","unstructured":"Eisert, J., Jacobs, K., Papadopoulos, P., Plenio, M.B.: Optimal local implementation of nonlocal quantum gates. Phys. Rev. A 62, 052317 (2000). https:\/\/doi.org\/10.1103\/PhysRevA.62.052317. https:\/\/link.aps.org\/doi\/10.1103\/PhysRevA.62.052317","DOI":"10.1103\/PhysRevA.62.052317"},{"key":"2_CR11","doi-asserted-by":"publisher","unstructured":"Feng, Y., Duan, R., Ying, M.: Bisimulation for quantum processes. ACM Trans. Program. Lang. Syst. 34(4) (2012). https:\/\/doi.org\/10.1145\/2400676.2400680","DOI":"10.1145\/2400676.2400680"},{"key":"2_CR12","doi-asserted-by":"publisher","unstructured":"Feng, Y., Li, S., Ying, M.: Verification of distributed quantum programs. ACM Trans. Comput. Logic 23(3) (2022). https:\/\/doi.org\/10.1145\/3517145","DOI":"10.1145\/3517145"},{"key":"2_CR13","doi-asserted-by":"publisher","unstructured":"Gay, S.J., Nagarajan, R.: Communicating quantum processes. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201905, pp. 145\u2013157. Association for Computing Machinery, New York (2005). https:\/\/doi.org\/10.1145\/1040305.1040318","DOI":"10.1145\/1040305.1040318"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Gibson-Robinson, T., Philip\u00a0Armstrong, A.B., Roscoe, A.: Fdr3 - a modern refinement checker for CSP. In: TACAS (2014)","DOI":"10.1007\/978-3-642-54862-8_13"},{"key":"2_CR15","doi-asserted-by":"publisher","unstructured":"Hietala, K., Rand, R., Li, L., Hung, S.H., Wu, X., Hicks, M.: A verified optimizer for quantum circuits. ACM Trans. Program. Lang. Syst. 45(3) (2023). https:\/\/doi.org\/10.1145\/3604630","DOI":"10.1145\/3604630"},{"key":"2_CR16","volume-title":"Communicating sequential processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Prentice-Hall Inc., Upper Saddle River (1985)"},{"key":"2_CR17","unstructured":"Inc, P., et al.: Distributed quantum computing in silicon (2024). https:\/\/arxiv.org\/abs\/2406.01704"},{"key":"2_CR18","unstructured":"IonQ: Ionq demonstrates remote ion-ion entanglement, a significant milestone in developing networked quantum systems at scale (2024). https:\/\/ionq.com\/news\/ionq-demonstrates-remote-ion-ion-entanglement-a-significant-milestone-in"},{"key":"2_CR19","doi-asserted-by":"publisher","unstructured":"Jorrand, P., Lalire, M.: Toward a quantum process algebra. In: Proceedings of the 1st Conference on Computing Frontiers, CF \u201904, pp. 111\u2013119. Association for Computing Machinery, New York (2004). https:\/\/doi.org\/10.1145\/977091.977108","DOI":"10.1145\/977091.977108"},{"key":"2_CR20","doi-asserted-by":"publisher","unstructured":"Li, L., Zhu, M., Cleaveland, R., Nicolellis, A., Lee, Y., Chang, L., Wu, X.: Qafny: a quantum-program verifier. In: Aldrich, J., Salvaneschi, G. (eds.) 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0313, pp. 24:1\u201324:31. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2024). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2024.24. https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.ECOOP.2024.24","DOI":"10.4230\/LIPIcs.ECOOP.2024.24"},{"key":"2_CR21","unstructured":"Ltd., F.S.E.: Failures-divergence refinement. FDR2 user manual. In: FDR2 User Manual (2010)"},{"key":"2_CR22","unstructured":"Main, D., et al.: Distributed quantum computing across an optical network link (2024). https:\/\/arxiv.org\/abs\/2407.00835"},{"key":"2_CR23","first-page":"135","volume":"15","author":"A Markov","year":"1906","unstructured":"Markov, A.: Rasprostranenie zakona bol\u2019shih chisel na velichiny, zavisyaschie drug ot druga. Izvestiya Fiziko-matematicheskogo obschestva pri Kazanskom universitete 15, 135\u2013156 (1906)","journal-title":"Izvestiya Fiziko-matematicheskogo obschestva pri Kazanskom universitete"},{"key":"2_CR24","unstructured":"Markov, A.: Extension of the limit theorems of probability theory to a sum of variables connected in a chain. In: The Notes of the Imperial Academy of Sciences of St. Petersburg VIII Series, Physio-Mathematical College, vol. XXII\/9 (1907)"},{"key":"2_CR25","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems","author":"R Milner","year":"1980","unstructured":"Milner, R.: A Calculus of Communicating Systems. Springer, Heidelberg (1980)"},{"key":"2_CR26","doi-asserted-by":"publisher","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, I. Inf. Comput. 100(1), 1\u201340 (1992). https:\/\/doi.org\/10.1016\/0890-5401(92)90008-4. https:\/\/www.sciencedirect.com\/science\/article\/pii\/0890540192900084","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"2_CR27","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"ML Puterman","year":"1994","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming, 1st edn. John Wiley & Sons Inc., Hoboken (1994)","edition":"1"},{"key":"2_CR28","doi-asserted-by":"publisher","unstructured":"Rigolin, G.: Quantum teleportation of an arbitrary two-qubit state and its relation to multipartite entanglement. Phys. Rev. A 71(3) (2005). https:\/\/doi.org\/10.1103\/physreva.71.032303","DOI":"10.1103\/physreva.71.032303"},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"Sangiorgi, D.: A theory of bisimulation for the pi-calculus. In: Best, E. (ed.) CONCUR. Lecture Notes in Computer Science, vol.\u00a0715, pp. 127\u2013142. Springer (1993)","DOI":"10.1007\/3-540-57208-2_10"},{"key":"2_CR30","unstructured":"Swayne, M.: Google is looking for proposals to push boundaries in distributed quantum computing (2024). https:\/\/thequantuminsider.com\/2024\/06\/18\/google-is-looking-for-proposals-to-push-boundaries-in-distributed-quantum-computing\/"},{"issue":"4","key":"2_CR31","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1109\/MC.2024.3360569","volume":"57","author":"W Tang","year":"2024","unstructured":"Tang, W., Martonosi, M.: Distributed quantum computing via integrating quantum and classical computing. Computer 57(4), 131\u2013136 (2024). https:\/\/doi.org\/10.1109\/MC.2024.3360569","journal-title":"Computer"},{"issue":"5886","key":"2_CR32","doi-asserted-by":"publisher","first-page":"802","DOI":"10.1038\/299802a0","volume":"299","author":"WK Wootters","year":"1982","unstructured":"Wootters, W.K., Zurek, W.H.: A single quantum cannot be cloned. Nature 299(5886), 802\u2013803 (1982). https:\/\/doi.org\/10.1038\/299802a0","journal-title":"Nature"},{"key":"2_CR33","doi-asserted-by":"publisher","unstructured":"Ying, M.: Floyd\u2013hoare logic for quantum programs. ACM Trans. Program. Lang. Syst. 33(6) (2012). https:\/\/doi.org\/10.1145\/2049706.2049708","DOI":"10.1145\/2049706.2049708"},{"issue":"6","key":"2_CR34","doi-asserted-by":"publisher","first-page":"728","DOI":"10.1109\/TC.2009.13","volume":"58","author":"M Ying","year":"2009","unstructured":"Ying, M., Feng, Y.: An algebraic language for distributed quantum computing. IEEE Trans. Comput. 58(6), 728\u2013743 (2009). https:\/\/doi.org\/10.1109\/TC.2009.13","journal-title":"IEEE Trans. Comput."},{"key":"2_CR35","doi-asserted-by":"publisher","unstructured":"Ying, M., Feng, Y., Duan, R., Ji, Z.: An algebra of quantum processes. ACM Trans. Comput. Logic 10(3) (2009). https:\/\/doi.org\/10.1145\/1507244.1507249","DOI":"10.1145\/1507244.1507249"},{"key":"2_CR36","unstructured":"Ying, M., Zhou, L., Li, Y.: Reasoning about parallel quantum programs (2018)"},{"key":"2_CR37","doi-asserted-by":"publisher","unstructured":"Ying, M., Zhou, L., Li, Y., Feng, Y.: A proof system for disjoint parallel quantum programs. Theor. Comput. Sci. 897, 164\u2013184 (2022). https:\/\/doi.org\/10.1016\/j.tcs.2021.10.025. https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0304397521006484","DOI":"10.1016\/j.tcs.2021.10.025"},{"key":"2_CR38","unstructured":"Zhang, Z., Ying, M.: Atomicity in distributed quantum computing (2024)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-28079-4_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:32:47Z","timestamp":1781191967000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-28079-4_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032280787","9783032280794"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-28079-4_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"12 June 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/nfm2026.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}