Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On the Relative Completeness of Satisfaction-based Quantum Hoare Logic

Xin Sun, Xingchi Su, Xiaoning Bian, Huiwen Wu

TL;DR

This work tackles the long-standing problem of achieving relative completeness for a satisfaction-based Quantum Hoare Logic with while-loops. It achieves this by a two-step strategy: first establishing a semantics and a proof system for Hoare triples with quantum programs and deterministic assertions, and then constructing a weakest preterm calculus via deterministic weakest preconditions to handle probabilistic expressions. The resulting QHL is shown to be relatively complete, and is extended to probabilistic assertions, enabling formal verification of quantum programs that involve both quantum operations and probabilistic behavior. The framework is demonstrated by formal verifications of Deutsch's algorithm and quantum teleportation, highlighting its potential to rigorously certify the correctness of quantum algorithms with loops and probabilistic features. The work also discusses future directions, including quantum relational Hoare logic and implementation considerations for broader quantum-program verification tasks.

Abstract

Quantum Hoare logic (QHL) is a formal verification tool specifically designed to ensure the correctness of quantum programs. There has been an ongoing challenge to achieve a relatively complete satisfaction-based QHL with while-loop since its inception in 2006. This paper presents a solution by proposing the first relatively complete satisfaction-based QHL with while-loop. The completeness is proved in two steps. First, we establish a semantics and proof system of Hoare triples with quantum programs and deterministic assertions. Then, by utilizing the weakest precondition of deterministic assertion, we construct the weakest preterm calculus of probabilistic expressions. The relative completeness of QHL is then obtained as a consequence of the weakest preterm calculus. Using our QHL, we formally verify the correctness of Deutsch's algorithm and quantum teleportation.

On the Relative Completeness of Satisfaction-based Quantum Hoare Logic

TL;DR

This work tackles the long-standing problem of achieving relative completeness for a satisfaction-based Quantum Hoare Logic with while-loops. It achieves this by a two-step strategy: first establishing a semantics and a proof system for Hoare triples with quantum programs and deterministic assertions, and then constructing a weakest preterm calculus via deterministic weakest preconditions to handle probabilistic expressions. The resulting QHL is shown to be relatively complete, and is extended to probabilistic assertions, enabling formal verification of quantum programs that involve both quantum operations and probabilistic behavior. The framework is demonstrated by formal verifications of Deutsch's algorithm and quantum teleportation, highlighting its potential to rigorously certify the correctness of quantum algorithms with loops and probabilistic features. The work also discusses future directions, including quantum relational Hoare logic and implementation considerations for broader quantum-program verification tasks.

Abstract

Quantum Hoare logic (QHL) is a formal verification tool specifically designed to ensure the correctness of quantum programs. There has been an ongoing challenge to achieve a relatively complete satisfaction-based QHL with while-loop since its inception in 2006. This paper presents a solution by proposing the first relatively complete satisfaction-based QHL with while-loop. The completeness is proved in two steps. First, we establish a semantics and proof system of Hoare triples with quantum programs and deterministic assertions. Then, by utilizing the weakest precondition of deterministic assertion, we construct the weakest preterm calculus of probabilistic expressions. The relative completeness of QHL is then obtained as a consequence of the weakest preterm calculus. Using our QHL, we formally verify the correctness of Deutsch's algorithm and quantum teleportation.
Paper Structure (21 sections, 19 theorems, 19 equations, 1 table)

This paper contains 21 sections, 19 theorems, 19 equations, 1 table.

Table of Contents

  1. Introduction
  2. Quantum Hoare logic with deterministic assertion
  3. Deterministic expressions and formulas
  4. Commands
  5. Proof system with deterministic assertions
  6. Soundness and completeness
  7. Quantum Hoare logic with probabilistic assertion
  8. Probabilistic formulas
  9. Proof system with probabilistic assertions
  10. Weakest preterms calculus and weakest precondition
  11. Proof system with probabilistic assertions
  12. Conclusion and future work
  13. Basics of quantum computation
  14. $n$-qubit states
  15. $n$-qubit unitary transformations
  16. ...and 6 more sections

Key Result

theorem 1

The proof system QHL$_d$ is sound, $i.e.$, for all deterministic formula $\phi$ and $\psi$ and command $C$, $\vdash\{\phi\}C\{\psi\}$ implies $\models\{\phi\}C\{\psi\}$.

Theorems & Definitions (57)

  • definition 1: Arithmetic expressions
  • definition 2: Boolean expressions
  • definition 3: Semantics of deterministic expressions
  • definition 4: Syntax of command expressions
  • definition 5: Semantics of command expressions
  • definition 6: Syntax of deterministic assertions
  • definition 7: Semantics of deterministic assertions
  • definition 8: Proof system QHL$_d$
  • theorem 1: Soundness
  • proof
  • ...and 47 more