Predicatet transformers for nondeterministic quantum programs

Wang, Xi; Gehnen, Christina; Katoen, Joost-Pieter; Unruh, Dominique

doi:10.18154/RWTH-2026-08566

Predicatet transformers for nondeterministic quantum programs

Wang, Xi

2026

Verantwortlichkeitsangabeby Xi Wang

ImpressumAachen : RWTH Aachen University 2026

Umfang1 Online-Ressource : Illustrationen

Bachelorarbeit, RWTH Aachen University, 2026

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University

Genehmigende Fakultät
Fak09

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

Tag der mündlichen Prüfung/Habilitation
2026-09-02

Online
DOI: 10.18154/RWTH-2026-08566
URL: https://publications.rwth-aachen.de/record/1041363/files/1041363.pdf

Einrichtungen

Lehrstuhl für Quanteninformationssysteme (Informatik 15) (125910)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Nondeterminism has been introduced into quantum programming languages to model, for example, unspecified behavior. Weakest precondition transformers provide a formal framework for reasoning about program correctness with respect to a given postcondition. This thesis combines these ideas by introducing demonic and angelic interpretations of nondeterminism for quantum programs, together with corresponding weakest liberal precondition transformers. To capture angelic nondeterminism in a qualitative setting, we introduce predicates represented by sets of subspaces, where each subspace is represented by a projection. Such a predicate is satisfied whenever the quantum state belongs to one of the represented subspaces. We show, however, that natural definitions of the weakest liberal precondition transformer based on these predicates do not behave as desired for measurements and loops in the demonic setting. For this reason, the demonic weakest liberal precondition transformer is restricted to singleton postconditions. We further investigate the corresponding non-liberal weakest precondition transformers using termination spaces. This yields transformer rules for all language constructs except loops, for which deriving a transformer rule remains an open problem. Finally, we show that the resulting weakest precondition variants have the same relations as in the classical case.

OpenAccess:
PDF