Analysis and Verification of Quantum Communication Protocols in UPPAAL

Nikolaj Rossander Kristensen; René Bødker Christensen; Kim Guldstrand Larsen; Marius Mikučionis; Loke Walsted; Jiri Srba

doi:10.1007/978-3-032-32537-2_18

Analysis and Verification of Quantum Communication Protocols in UPPAAL

Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Konferenceartikel i proceeding › Forskning › peer review

Abstract

We introduce a formal modeling methodology to analyze quantum communication protocols in the tool Uppaal. Our approach encodes quantum states, operations, and measurements into Uppaal timed automata with data extensions and external C++ function calls, enabling both exhaustive verification in the ideal (noiseless) case and statistical model checking for realistic noisy scenarios. We apply our framework to the Beyond Superdense Coding protocol—a time-slotted variant of superdense coding—combined with quantum entanglement distillation, and demonstrate that Uppaal can deal with these protocols even under complex timing and decoherence constraints.

Originalsprog	Engelsk
Titel	International Conference on Computer Aided Verification
Redaktører	Eva Darulova, Anthony W. Lin, Philipp Rümmer
Antal sider	15
Vol/bind	16684
Udgivelsessted	Springer Nature Proceedings Computer Science
Forlag	Springer Nature
Publikationsdato	24 jul. 2026
Sider	372-386
ISBN (Trykt)	978-3-032-32536-5
ISBN (Elektronisk)	978-3-032-32537-2
DOI	https://doi.org/10.1007/978-3-032-32537-2_18
Status	Udgivet - 24 jul. 2026
Begivenhed	Computer Aided Verification - Lisbon, Portugal Varighed: 26 jul. 2026 → 29 jul. 2026 https://conferences.i-cav.org/2026/

Konference

Konference	Computer Aided Verification
Land/Område	Portugal
By	Lisbon
Periode	26/07/2026 → 29/07/2026
Internetadresse	https://conferences.i-cav.org/2026/

Emneord

Quantum communication
UPPAAL
Model Checking

Adgang til dokumentet

10.1007/978-3-032-32537-2_18

AUB Link

Søg efter materialet i Aalborg Universitetsbiblioteks søgemaskine

Andre filer og links

Link to publication in Scopus

Citationsformater

Kristensen, Nikolaj Rossander ; Christensen, René Bødker ; Larsen, Kim Guldstrand et al. / Analysis and Verification of Quantum Communication Protocols in UPPAAL. International Conference on Computer Aided Verification. red. / Eva Darulova ; Anthony W. Lin ; Philipp Rümmer. Bind 16684 Springer Nature Proceedings Computer Science : Springer Nature, 2026. s. 372-386

@inproceedings{8fce15299ba44dc38cc7fb5016664dd7,

title = "Analysis and Verification of Quantum Communication Protocols in UPPAAL",

abstract = "We introduce a formal modeling methodology to analyze quantum communication protocols in the tool Uppaal. Our approach encodes quantum states, operations, and measurements into Uppaal timed automata with data extensions and external C++ function calls, enabling both exhaustive verification in the ideal (noiseless) case and statistical model checking for realistic noisy scenarios. We apply our framework to the Beyond Superdense Coding protocol{\textemdash}a time-slotted variant of superdense coding{\textemdash}combined with quantum entanglement distillation, and demonstrate that Uppaal can deal with these protocols even under complex timing and decoherence constraints.",

keywords = "Quantum communication, UPPAAL, Model Checking",

author = "Kristensen, \{Nikolaj Rossander\} and Christensen, \{Ren{\'e} B{\o}dker\} and Larsen, \{Kim Guldstrand\} and Marius Miku{\v c}ionis and Loke Walsted and Jiri Srba",

year = "2026",

month = jul,

day = "24",

doi = "10.1007/978-3-032-32537-2\_18",

language = "English",

isbn = "978-3-032-32536-5",

volume = "16684",

pages = "372--386",

editor = "Eva Darulova and Lin, \{Anthony W.\} and Philipp R{\"u}mmer",

booktitle = "International Conference on Computer Aided Verification",

publisher = "Springer Nature",

address = "United States",

note = "Computer Aided Verification ; Conference date: 26-07-2026 Through 29-07-2026",

url = "https://conferences.i-cav.org/2026/",

}

Kristensen, NR , Christensen, RB , Larsen, KG , Mikučionis, M , Walsted, L & Srba, J 2026, Analysis and Verification of Quantum Communication Protocols in UPPAAL. i E Darulova, AW Lin & P Rümmer (red), International Conference on Computer Aided Verification. bind 16684, Springer Nature, Springer Nature Proceedings Computer Science, s. 372-386, Computer Aided Verification , Lisbon, Portugal, 26/07/2026. https://doi.org/10.1007/978-3-032-32537-2_18

Analysis and Verification of Quantum Communication Protocols in UPPAAL. / Kristensen, Nikolaj Rossander ; Christensen, René Bødker ; Larsen, Kim Guldstrand et al.
International Conference on Computer Aided Verification. red. / Eva Darulova; Anthony W. Lin; Philipp Rümmer. Bind 16684 Springer Nature Proceedings Computer Science: Springer Nature, 2026. s. 372-386.

Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Konferenceartikel i proceeding › Forskning › peer review

TY - GEN

T1 - Analysis and Verification of Quantum Communication Protocols in UPPAAL

AU - Kristensen, Nikolaj Rossander

AU - Christensen, René Bødker

AU - Larsen, Kim Guldstrand

AU - Mikučionis, Marius

AU - Walsted, Loke

AU - Srba, Jiri

PY - 2026/7/24

Y1 - 2026/7/24

N2 - We introduce a formal modeling methodology to analyze quantum communication protocols in the tool Uppaal. Our approach encodes quantum states, operations, and measurements into Uppaal timed automata with data extensions and external C++ function calls, enabling both exhaustive verification in the ideal (noiseless) case and statistical model checking for realistic noisy scenarios. We apply our framework to the Beyond Superdense Coding protocol—a time-slotted variant of superdense coding—combined with quantum entanglement distillation, and demonstrate that Uppaal can deal with these protocols even under complex timing and decoherence constraints.

AB - We introduce a formal modeling methodology to analyze quantum communication protocols in the tool Uppaal. Our approach encodes quantum states, operations, and measurements into Uppaal timed automata with data extensions and external C++ function calls, enabling both exhaustive verification in the ideal (noiseless) case and statistical model checking for realistic noisy scenarios. We apply our framework to the Beyond Superdense Coding protocol—a time-slotted variant of superdense coding—combined with quantum entanglement distillation, and demonstrate that Uppaal can deal with these protocols even under complex timing and decoherence constraints.

KW - Quantum communication

KW - UPPAAL

KW - Model Checking

UR - https://www.scopus.com/pages/publications/105047071125

U2 - 10.1007/978-3-032-32537-2_18

DO - 10.1007/978-3-032-32537-2_18

M3 - Article in proceeding

SN - 978-3-032-32536-5

VL - 16684

SP - 372

EP - 386

BT - International Conference on Computer Aided Verification

A2 - Darulova, Eva

A2 - Lin, Anthony W.

A2 - Rümmer, Philipp

PB - Springer Nature

CY - Springer Nature Proceedings Computer Science

T2 - Computer Aided Verification

Y2 - 26 July 2026 through 29 July 2026

ER -

Analysis and Verification of Quantum Communication Protocols in UPPAAL

Abstract

Konference

Emneord

Adgang til dokumentet

AUB Link

Andre filer og links

Fingeraftryk

Citationsformater