h1

TY  - THES
AU  - Kierner, Kaleb
TI  - Modeling non-deterministic quantum programs for model checking
PB  - RWTH Aachen University
VL  - Bachelorarbeit
CY  - Aachen
M1  - RWTH-2025-09031
SP  - 1 Online-Ressource : Illustrationen
PY  - 2025
N1  - Veröffentlicht auf dem Publikationsserver der RWTH Aachen University
N1  - Bachelorarbeit, RWTH Aachen University, 2025
AB  - 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.
LB  - PUB:(DE-HGF)2
DO  - DOI:10.18154/RWTH-2025-09031
UR  - https://publications.rwth-aachen.de/record/1020481
ER  -