h1

h2

h3

h4

h5
h6


001     1020481
005     20251105054627.0
024 7 _ |2 datacite_doi
|a 10.18154/RWTH-2025-09031
037 _ _ |a RWTH-2025-09031
041 _ _ |a English
082 _ _ |a 004
100 1 _ |0 P:(DE-82)1020781
|a Kierner, Kaleb
|b 0
|u rwth
245 _ _ |a Modeling non-deterministic quantum programs for model checking
|c Kaleb Kierner
|h online
260 _ _ |a Aachen
|b RWTH Aachen University
|c 2025
300 _ _ |a 1 Online-Ressource : Illustrationen
336 7 _ |0 2
|2 EndNote
|a Thesis
336 7 _ |0 PUB:(DE-HGF)2
|2 PUB:(DE-HGF)
|a Bachelor Thesis
|b bachelor
|m bachelor
336 7 _ |2 BibTeX
|a MASTERSTHESIS
336 7 _ |2 DRIVER
|a bachelorThesis
336 7 _ |2 DataCite
|a Output Types/Supervised Student Publication
336 7 _ |2 ORCID
|a SUPERVISED_STUDENT_PUBLICATION
500 _ _ |a Veröffentlicht auf dem Publikationsserver der RWTH Aachen University
502 _ _ |a Bachelorarbeit, RWTH Aachen University, 2025
|b Bachelorarbeit
|c RWTH Aachen University
|d 2025
|g Fak01
|o 2025-09-22
520 3 _ |l ger
520 _ _ |a 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.
|l eng
591 _ _ |a Germany
700 1 _ |0 P:(DE-82)IDM00048
|a Katoen, Joost-Pieter
|b 1
|e Thesis advisor
|u rwth
700 1 _ |0 P:(DE-82)IDM06461
|a Unruh, Dominique
|b 2
|e Thesis advisor
|u rwth
700 1 _ |0 P:(DE-82)IDM05193
|a Gehnen, Christina
|b 3
|e Consultant
|u rwth
856 4 _ |u https://publications.rwth-aachen.de/record/1020481/files/1020481.pdf
|y OpenAccess
909 C O |o oai:publications.rwth-aachen.de:1020481
|p openaire
|p open_access
|p VDB
|p driver
|p dnbdelivery
910 1 _ |0 I:(DE-588b)36225-6
|6 P:(DE-82)1020781
|a RWTH Aachen
|b 0
|k RWTH
910 1 _ |0 I:(DE-588b)36225-6
|6 P:(DE-82)IDM00048
|a RWTH Aachen
|b 1
|k RWTH
910 1 _ |0 I:(DE-588b)36225-6
|6 P:(DE-82)IDM06461
|a RWTH Aachen
|b 2
|k RWTH
910 1 _ |0 I:(DE-588b)36225-6
|6 P:(DE-82)IDM05193
|a RWTH Aachen
|b 3
|k RWTH
914 1 _ |y 2025
915 _ _ |0 StatID:(DE-HGF)0510
|2 StatID
|a OpenAccess
920 1 _ |0 I:(DE-82)121310_20140620
|k 121310
|l Lehrstuhl für Softwaremodellierung und Verifikation (Informatik 2)
|x 0
920 1 _ |0 I:(DE-82)120000_20140620
|k 120000
|l Fachgruppe Informatik
|x 1
980 1 _ |a FullTexts
980 _ _ |a I:(DE-82)120000_20140620
980 _ _ |a I:(DE-82)121310_20140620
980 _ _ |a UNRESTRICTED
980 _ _ |a VDB
980 _ _ |a bachelor


LibraryCollectionCLSMajorCLSMinorLanguageAuthor
Marc 21