Generalised quantum weakest preconditions

TL;DR

This paper extends the quantum weakest precondition framework to include general quantum predicates as POVMs, applicable in infinite-dimensional spaces and for non-completely positive transformations, broadening the theoretical foundation of quantum program verification.

Contribution

It introduces the most general notion of quantum predicate as POVM and extends weakest precondition results to infinite dimensions and non-completely positive transformations.

Findings

Extended weakest precondition to POVMs as quantum predicates

Applicable in infinite-dimensional quantum systems

Valid for positive, not necessarily completely positive, transformations

Abstract

Generalisation of the quantum weakest precondition result of D'Hondt and Panangaden is presented. In particular the most general notion of quantum predicate as positive operator valued measure (POVM) is introduced. The previously known quantum weakest precondition result has been extended to cover the case of POVM playing the role of a quantum predicate. Additionally, our result is valid in infinite dimension case and also holds for a quantum programs defined as a positive but not necessary completely positive transformations of a quantum states.