% IMPORTANT: The following is UTF-8 encoded. This means that in the presence
% of non-ASCII characters, it will not work with BibTeX 0.99 or older.
% Instead, you should use an up-to-date BibTeX implementation like “bibtex8” or
% “biber”.
@MASTERSTHESIS{Kierner:1020481,
author = {Kierner, Kaleb},
othercontributors = {Katoen, Joost-Pieter and Unruh, Dominique and Gehnen,
Christina},
title = {{M}odeling non-deterministic quantum programs for model
checking},
school = {RWTH Aachen University},
type = {Bachelorarbeit},
address = {Aachen},
publisher = {RWTH Aachen University},
reportid = {RWTH-2025-09031},
pages = {1 Online-Ressource : Illustrationen},
year = {2025},
note = {Veröffentlicht auf dem Publikationsserver der RWTH Aachen
University; Bachelorarbeit, RWTH Aachen University, 2025},
abstract = {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.},
cin = {121310 / 120000},
ddc = {004},
cid = {$I:(DE-82)121310_20140620$ / $I:(DE-82)120000_20140620$},
typ = {PUB:(DE-HGF)2},
doi = {10.18154/RWTH-2025-09031},
url = {https://publications.rwth-aachen.de/record/1020481},
}
guest ::