Gast ::
001020481 001__ 1020481 001020481 005__ 20251105054627.0 001020481 0247_ $$2datacite_doi$$a10.18154/RWTH-2025-09031 001020481 037__ $$aRWTH-2025-09031 001020481 041__ $$aEnglish 001020481 082__ $$a004 001020481 1001_ $$0P:(DE-82)1020781$$aKierner, Kaleb$$b0$$urwth 001020481 245__ $$aModeling non-deterministic quantum programs for model checking$$cKaleb Kierner$$honline 001020481 260__ $$aAachen$$bRWTH Aachen University$$c2025 001020481 300__ $$a1 Online-Ressource : Illustrationen 001020481 3367_ $$02$$2EndNote$$aThesis 001020481 3367_ $$0PUB:(DE-HGF)2$$2PUB:(DE-HGF)$$aBachelor Thesis$$bbachelor$$mbachelor 001020481 3367_ $$2BibTeX$$aMASTERSTHESIS 001020481 3367_ $$2DRIVER$$abachelorThesis 001020481 3367_ $$2DataCite$$aOutput Types/Supervised Student Publication 001020481 3367_ $$2ORCID$$aSUPERVISED_STUDENT_PUBLICATION 001020481 500__ $$aVeröffentlicht auf dem Publikationsserver der RWTH Aachen University 001020481 502__ $$aBachelorarbeit, RWTH Aachen University, 2025$$bBachelorarbeit$$cRWTH Aachen University$$d2025$$gFak01$$o2025-09-22 001020481 5203_ $$lger 001020481 520__ $$aQuantum 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.$$leng 001020481 591__ $$aGermany 001020481 7001_ $$0P:(DE-82)IDM00048$$aKatoen, Joost-Pieter$$b1$$eThesis advisor$$urwth 001020481 7001_ $$0P:(DE-82)IDM06461$$aUnruh, Dominique$$b2$$eThesis advisor$$urwth 001020481 7001_ $$0P:(DE-82)IDM05193$$aGehnen, Christina$$b3$$eConsultant$$urwth 001020481 8564_ $$uhttps://publications.rwth-aachen.de/record/1020481/files/1020481.pdf$$yOpenAccess 001020481 909CO $$ooai:publications.rwth-aachen.de:1020481$$popenaire$$popen_access$$pVDB$$pdriver$$pdnbdelivery 001020481 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)1020781$$aRWTH Aachen$$b0$$kRWTH 001020481 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM00048$$aRWTH Aachen$$b1$$kRWTH 001020481 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM06461$$aRWTH Aachen$$b2$$kRWTH 001020481 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM05193$$aRWTH Aachen$$b3$$kRWTH 001020481 9141_ $$y2025 001020481 915__ $$0StatID:(DE-HGF)0510$$2StatID$$aOpenAccess 001020481 9201_ $$0I:(DE-82)121310_20140620$$k121310$$lLehrstuhl für Softwaremodellierung und Verifikation (Informatik 2)$$x0 001020481 9201_ $$0I:(DE-82)120000_20140620$$k120000$$lFachgruppe Informatik$$x1 001020481 961__ $$c2025-11-04T10:23:21.610114$$x2025-10-28T15:02:30.042473$$z2025-11-04T10:23:21.610114 001020481 9801_ $$aFullTexts 001020481 980__ $$aI:(DE-82)120000_20140620 001020481 980__ $$aI:(DE-82)121310_20140620 001020481 980__ $$aUNRESTRICTED 001020481 980__ $$aVDB 001020481 980__ $$abachelor