{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:10:33Z","timestamp":1784200233160,"version":"3.55.0"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T00:00:00Z","timestamp":1759968000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100003475","name":"Hasler Stiftung","doi-asserted-by":"publisher","award":["23086, 2024-09-27-175"],"award-info":[{"award-number":["23086, 2024-09-27-175"]}],"id":[{"id":"10.13039\/501100003475","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA95502310361, FA95502310406"],"award-info":[{"award-number":["FA95502310361, FA95502310406"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-22-EXES-0013 (project STeP2\/F4C)"],"award-info":[{"award-number":["ANR-22-EXES-0013 (project STeP2\/F4C)"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>\n                    Quantum networks have capabilities that are impossible to achieve using only classical information. They connect quantum capable nodes, with their fundamental unit of communication being the\n                    <jats:italic toggle=\"yes\">Bell pair<\/jats:italic>\n                    , a pair of entangled quantum bits. Due to the nature of quantum phenomena, Bell pairs are fragile and difficult to transmit over long distances, thus requiring a network of repeaters along with dedicated hardware and software to ensure the desired results. The intrinsic challenges associated with quantum networks, such as competition over shared resources and high probabilities of failure, require quantitative reasoning about quantum network protocols. This paper develops PBKAT, an expressive language for specification, verification and optimization of quantum network protocols for Bell pair distribution. Our language is equipped with primitives for expressing probabilistic and possibilistic behaviors, and with semantics modeling protocol executions. We establish the properties of PBKAT\u2019s semantics, which we use for quantitative analysis of protocol behavior. We further implement a tool to automate PBKAT\u2019s usage, which we evaluated on real-world protocols drawn from the literature. Our results indicate that PBKAT is well suited for both expressing real-world quantum network protocols and reasoning about their quantitative properties.\n                  <\/jats:p>","DOI":"10.1145\/3763135","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"2367-2395","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A Language for Quantifying Quantum Network Behavior"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4493-2999","authenticated-orcid":false,"given":"Anita","family":"Buckley","sequence":"first","affiliation":[{"name":"USI Lugano, Lugano, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6673-1143","authenticated-orcid":false,"given":"Pavel","family":"Chuprikov","sequence":"additional","affiliation":[{"name":"T\u00e9l\u00e9com Paris, Palaiseau, France"},{"name":"Institut Polytechnique de Paris, Palaiseau, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1097-2367","authenticated-orcid":false,"given":"Rodrigo","family":"Otoni","sequence":"additional","affiliation":[{"name":"USI Lugano, Lugano, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2825-6660","authenticated-orcid":false,"given":"Robert","family":"Soul\u00e9","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6842-5505","authenticated-orcid":false,"given":"Robert","family":"Rand","sequence":"additional","affiliation":[{"name":"University of Chicago, Chicago, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3864-9078","authenticated-orcid":false,"given":"Patrick","family":"Eugster","sequence":"additional","affiliation":[{"name":"USI Lugano, Lugano, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_2_2_1","unstructured":"Amar Abane Michael Cubeddu Van Sy Mai and Abdella Battou. 2024. Entanglement Routing in Quantum Networks: A Comprehensive Survey. arXiv:2408.01234 https:\/\/arxiv.org\/abs\/2408.01234"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535862"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysicsPhysiqueFizika.1.195"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","unstructured":"Filippo Bonchi Ana Sokolova and Valeria Vignudelli. 2021. The Theory of Traces for Systems with Nondeterminism and Probability. In Proceedings of the 34th ACM\/IEEE Symposium on Logic in Computer Science. 1\u201314. doi:10.1109\/LICS.2019.8785673","DOI":"10.1109\/LICS.2019.8785673"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-18(2:21)2022"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.81.5932"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","unstructured":"Anita Buckley Pavel Chuprikov Rodrigo Otoni Robert Soul\u00e9 Robert Rand and Patrick Eugster. 2024. An Algebraic Language for Specifying Quantum Networks. Proceedings of the ACM on Programmming Languages 8 PLDI (2024) 1\u201323. doi:10.1145\/3656430","DOI":"10.1145\/3656430"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"e_1_3_2_10_1","doi-asserted-by":"crossref","unstructured":"Christophe Chareton S\u00e9bastien Bardin Dongho Lee Beno\u00eet Valiron Renaud Vilmart and Zhaowei Xu. 2022. Formal Methods for Quantum Programs: A Survey. arXiv:2109.06493","DOI":"10.1201\/9781003090052-7"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","unstructured":"Pavel Chuprikov. 2025. Artifact for \u201cA Language for Quantifying Quantum Network Behavior\u201d. doi:10.5281\/zenodo.16915684","DOI":"10.5281\/zenodo.16915684"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1038\/s42005-021-00647-8"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1088\/2058-9565\/aad56e"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/TQE.2021.3092395"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","unstructured":"C. Delle Donne M. Iuliano B. van der Vecht G. M. Ferreira H. Jirovsk\u00e1 T. J. W. van der Steenhoven A. Dahlberg M. Skrzypczyk D. Fioretto M. Teller P. Filippov A. R.-P. Montblanch J. Fischer H. B. van Ommen N. Demetriou D. Leichtle L. Music H. Ollivier I. te Raa W. Kozlowski T. H. Taminiau P. Pawe\u0142czak T. E. Northup R. Hanson and S. Wehner. 2025. An Operating System for Executing Applications on Quantum Network Nodes. Nature 639 8054 (2025) 321\u2013328. doi:10.1038\/s41586-025-08704-w","DOI":"10.1038\/s41586-025-08704-w"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.62.062314"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","unstructured":"Nate Foster Dexter Kozen Konstantinos Mamouras Mark Reitblatt and Alexandra Silva. 2016. Probabilistic NetKAT. In Proceedings of the 25th European Symposium on Programming Languages and Systems. 282\u2013309. doi:10.1007\/978-3-662-49498-1_12","DOI":"10.1007\/978-3-662-49498-1_12"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3524455"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.97300"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434318"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2022.109092"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.05.023"},{"key":"e_1_3_2_23_1","unstructured":"Keith Kenemer. 2024. Error Correction in Quantum Networks. Aliro Technologies. https:\/\/www.aliroquantum.com\/blog\/an-overview-of-quantan-overview-of-quantum-error-correction-in-entanglement-based-networksum-error-correction-in-entanglement-based-networks"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-024-07252-z"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","unstructured":"Wojciech Kozlowski and Stephanie Wehner. 2019. Towards Large-Scale Quantum Networks. In Proceedings of the 6th ACM International Conference on Nanoscale Computing and Communication. 1\u20137. doi:10.1145\/3345312.3345497","DOI":"10.1145\/3345312.3345497"},{"key":"e_1_3_2_26_1","doi-asserted-by":"crossref","unstructured":"Wojciech Kozlowski Stephanie Wehner Rodney Van Meter Bruno Rijsman Angela Sara Cacciapuoti Marcello Caleffi and Shota Nagayama. 2023. Architectural Principles for a Quantum Internet. RFC 9340 (https:\/\/www.rfc-editor.org\/info\/rfc9340).","DOI":"10.17487\/RFC9340"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3624483"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/COMST.2024.3361662"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/COMST.2023.3294240"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-024-07308-0"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/b138392"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","unstructured":"Matteo Mio Ralph Sarkis and Valeria Vignudelli. 2021. Combining Nondeterminism Probability and Termination: Equational and Metric Reasoning. In Proceedings of the 36th ACM\/IEEE Symposium on Logic in Computer Science. 1\u201314. doi:10.1109\/LICS52264.2021.9470717","DOI":"10.1109\/LICS52264.2021.9470717"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","unstructured":"Michael W. Mislove. 2006. On Combining Probability and Nondeterminism. Electronic Notes in Theoretical Computer Science 162 (2006) 261\u2013265. doi:10.1016\/j.entcs.2005.12.113 Proceedings of the Workshop \u201cEssays on Algebraic Process Calculi\u201d (APC 25).","DOI":"10.1016\/j.entcs.2005.12.113"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45099-3_17"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511976667"},{"key":"e_1_3_2_37_1","first-page":"9","article-title":"Routing Entanglement in the Quantum Internet","volume":"25","author":"Pant Mihir","year":"2019","unstructured":"Mihir Pant, Hari Krovi, Don Towsley, Leandros Tassiulas, Liang Jiang, Prithwish Basu, Dirk Englund, and Saikat Guha. 2019. Routing Entanglement in the Quantum Internet. npj Quantum Information 5, 25 (2019), 1\u20139.","journal-title":"npj Quantum Information 5"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","unstructured":"S. Pirandola U. L. Andersen L. Banchi M. Berta D. Bunandar R. Colbeck D. Englund T. Gehring C. Lupo C. Ottaviani J. L. Pereira M. Razavi J. Shamsul Shaari M. Tomamichel V. C. Usenko G. Vallone P. Villoresi and P. Wallden. 2020. Advances in Quantum Cryptography. Advances in Optics and Photonics 12 4 (2020) 1012\u20131236. doi:10.1364\/AOP.361502","DOI":"10.1364\/AOP.361502"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1126\/science.abg1919"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.07.009"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-13-0659-4"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41534-021-00501-3"},{"key":"e_1_3_2_43_1","unstructured":"Robert Rand and Steve Zdancewic. 2016. Models for Probabilistic Programs with an Adversary. Workshop on Probabilistic Programming Semantics. http:\/\/pps2016.soic.indiana.edu\/2015\/12\/16\/adversaries"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","unstructured":"Wojciech R\u00f3\u017cowski Tobias Kapp\u00e9 Dexter Kozen Todd Schmid and Alexandra Silva. 2023. Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity. In 50th International Colloquium on Automata Languages and Programming (ICALP 2023) (Leibniz International Proceedings in Informatics (LIPIcs) Vol. 261) Kousha Etessami Uriel Feige and Gabriele Puppis (Eds.). Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik Dagstuhl Germany 136:1\u2013136:20. doi:10.4230\/LIPIcs.ICALP.2023.136","DOI":"10.4230\/LIPIcs.ICALP.2023.136"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","unstructured":"Ryosuke Satoh Michal Hajdu\u0161ek Naphan Benchasattabuse Shota Nagayama Kentaro Teramoto Takaaki Matsuo Sara Ayman Metwalli Takahiko Satoh Shigeya Suzuki and Rodney Van Meter. 2022. QuISP: a Quantum Internet Simulation Package. In 2022 IEEE International Conference on Quantum Computing and Engineering (QCE). IEEE 354\u2013365. doi:10.1109\/QCE53715.2022.00048","DOI":"10.1109\/QCE53715.2022.00048"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","unstructured":"Steffen Smolka Nate Foster Justin Hsu Tobias Kapp\u00e9 Dexter Kozen and Alexandra Silva. 2019a. Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time. Proceedings of the ACM on Programming Languages 4 POPL (2019) 1\u201328. doi:10.1145\/3371129","DOI":"10.1145\/3371129"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","unstructured":"Steffen Smolka Praveen Kumar David M. Kahn Nate Foster Justin Hsu Dexter Kozen and Alexandra Silva. 2019b. Scalable Verification of Probabilistic Networks. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. 190\u2013203. doi:10.1145\/3314221.3314639","DOI":"10.1145\/3314221.3314639"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1126\/sciadv.adp6442"},{"key":"e_1_3_2_49_1","unstructured":"Don Towsley. 2021. The Quantum Internet: Recent Advances and Challenges. Keynote at the 29th IEEE International Conference on Network Protocols. https:\/\/icnp21.cs.ucr.edu"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785779"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/79173.79181"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/MCOM.2013.6576340"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","unstructured":"Rodney Van Meter Joe Touch and Clare Horsman. 2011. Recursive Quantum Repeater Networks. Progress in Informatics 8 (2011) 65\u201379. doi:10.2201\/NiiPi.2011.8.8","DOI":"10.2201\/NiiPi.2011.8.8"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505005074"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","unstructured":"Jana Wagemaker Marcello Bonsangue Tobias Kapp\u00e9 Jurriaan Rot and Alexandra Silva. 2019. Completeness and Incompleteness of Synchronous Kleene Algebra. In Proceedings of the 13th International Conference on Mathematics of Program Construction. 385\u2013413. doi:10.1007\/978-3-030-33636-3_14","DOI":"10.1007\/978-3-030-33636-3_14"},{"key":"e_1_3_2_56_1","doi-asserted-by":"crossref","unstructured":"Chonggang Wang Akbar Rahman Ruidong Li Melchior Aelmans and Kaushik Chakraborty. 2023. Application Scenarios for the Quantum Internet. Technical Report. Internet Engineering Task Force. https:\/\/datatracker.ietf.org\/doc\/draft-irtf-qirg-quantum-internet-use-cases\/16","DOI":"10.17487\/RFC9583"},{"key":"e_1_3_2_57_1","doi-asserted-by":"publisher","DOI":"10.1126\/science.aam9288"},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","DOI":"10.1088\/2058-9565\/ac22f6"},{"key":"e_1_3_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_3_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571222"},{"key":"e_1_3_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314584"},{"key":"e_1_3_2_62_1","unstructured":"Noam Zilberstein Dexter Kozen Alexandra Silva and Joseph Tassarotti. 2024. A Demonic Outcome Logic for Randomized Nondeterminism. arXiv:2410.22540 https:\/\/arxiv.org\/pdf\/2410.22540"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763135","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763135","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:12:19Z","timestamp":1784196739000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763135"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":61,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763135"],"URL":"https:\/\/doi.org\/10.1145\/3763135","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-25","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}