Modeling non-deterministic quantum programs for model checking

Kierner, Kaleb; Gehnen, Christina; Unruh, Dominique; Katoen, Joost-Pieter

doi:10.18154/RWTH-2025-09031

Modeling non-deterministic quantum programs for model checking

Kierner, Kaleb^RWTH*

2025

VerantwortlichkeitsangabeKaleb Kierner

ImpressumAachen : RWTH Aachen University 2025

Umfang1 Online-Ressource : Illustrationen

Bachelorarbeit, RWTH Aachen University, 2025

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Katoen, Joost-Pieter (Thesis advisor)^RWTH* ; Unruh, Dominique (Thesis advisor)^RWTH* ; Gehnen, Christina (Consultant)^RWTH*

Tag der mündlichen Prüfung/Habilitation
2025-09-22

Online
DOI: 10.18154/RWTH-2025-09031
URL: https://publications.rwth-aachen.de/record/1020481/files/1020481.pdf

Einrichtungen

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Quantum programming introduces both probabilistic and non-deterministic behavior, making formal verification a challenging task. This work develops a framework for modeling non-deterministic quantum programs using Markov Decision Processes (MDPs). Each program configuration is represented as a combination of the remaining program and its quantum state, while transitions capture both quantum evolution and non-deterministic branching. We define operational semantics for quantum programs in terms of MDPs and prove their equivalence to established denotational semantics. This equivalence ensures consistency between high-level mathematical descriptions and executable models. The approach enables the application of model-checking techniques, originally designed for classical probabilistic systems, to quantum programs. Our results show that MDPs provide a foundation for verifying properties of non-deterministic quantum programs.

OpenAccess:
PDF