Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

arXiv:1911.12557

Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs (Extended Version)

Junyi Liu, Zhou, Li, Gilles Barthe, Mingsheng Ying

Published Nov 28, 2019• 0 citations
arXivHTMLPDF

Abstract

We study expected runtimes for quantum programs. Inspired by recent work on probabilistic programs, we first define expected runtime as a generalisation of quantum weakest precondition. Then, we show that the expected runtime of a quantum program can be represented as the expectation of an observable (in physics). A method for computing the expected runtimes of quantum programs in finite-dimensional state spaces is developed. Several examples are provided as applications of this method, including computing the expected runtime of quantum Bernoulli Factory -- a quantum algorithm for generating random numbers. In particular, using our new method, an open problem of computing the expected runtime of quantum random walks introduced by Ambainis et al. (STOC 2001) is solved.

DOI
10.48550/arxiv.1911.12557

Related papers

Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs

Junyi Liu, Li Zhou, Gilles Barthe +1 more

We study expected runtimes for quantum programs. Inspired by recent work on probabilistic programs, we first define expected runtime as a generalisation of quantum weakest precondition. Then, we show that the expected runtime of a quantum program can be represented as the expectation of an observable (in physics). A method for computing the expected runtimes of quantum programs in finite-dimensional state spaces is developed. Several examples are provided as applications of this method, including computing the expected runtime of quantum Bernoulli Factory – a quantum algorithm for generating random numbers. In particular, using our new method, an open problem of computing the expected runtime of quantum random walks introduced by Ambainis et al. (STOC 2001) is solved.

ACM/IEEE Symposium on Logic in Computer Science (LICS)•Aug 2, 2022•17 citations

Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs

Junyi Liu, Li Zhou, Gilles Barthe +1 more

We study expected runtimes for quantum programs. Inspired by recent work on probabilistic programs, we first define expected runtime as a generalisation of quantum weakest precondition . Then, we show that the expected runtime of a quantum program should be represented as the expectation of an observable (in physics). A method for computing the expected runtimes of quantum programs in finite-dimensional state spaces is developed. Several examples are provided as applications of this method, including computing the expected runtime of quantum Bernoulli Factory – a quantum algorithm for generating random numbers. In particular, using our new method, an open problem of computing the expected runtime of quantum random walks introduced by Ambainis et al. ( STOC 2001) is solved.

Journal of the ACM•May 6, 2025•1 citation

Quantum Weakest Preconditions Revisited: Pre-expectations for Expected Runtime Analysis

Christina Gehnen, Dominique Unruh, Joost-Pieter Katoen

Quantum weakest preconditions are a fundamental tool for program verification of quantum programs. Many variations have been reported in the literature. We revisit quantum weakest preconditions from the perspective of expected runtime analysis of quantum programs and introduce a novel pre-expectation framework that enables to reason about the preconditions of quantum programs without the need of an upper bound. This is particularly interesting for quantum programs involving reward statements. The overall goal is to analyze runtime behavior even in the case of programs with potentially infinite expected runtime. This paper presents several ways to do so, e.g., a program transformation such that the expected runtime of a quantum program can be expressed using the weakest pre-expectation calculus with rewards.

cs.LOCross-listedarXiv:2607.12532•Jul 15, 2026•0 citations

Expected Runtime of Quantum Programs

Junyi Liu, Li Zhou, Mingsheng Ying

Building upon recent work on probabilistic programs, we formally define the notion of expected runtime for quantum programs. A representation of the expected runtimes of quantum programs is introduced with an interpretation as an observable in physics. A method for computing the expected runtimes of quantum programs in finite-dimensional state spaces is developed. Several examples are provided as applications of this method; in particular, an open problem of computing the expected runtime of quantum random walks is solved using our method.

•Nov 28, 2019•1 citation

Runtime Analysis of Quantum Programs: A Formal Approach

Federico Olmedo, Alejandro Díaz-Caro

In this abstract we study the resource consumption of quantum programs. Specifically, we focus on the expected runtime of programs and, inspired by recent methods for probabilistic programs, we develop a calculus à la weakest precondition to formally and systematically derive the (exact) expected runtime of quantum programs. Notably, the calculus admits a notion of loop runtime invariant that can be readily used to derive upper bounds of their runtime. Finally, we show the applicability of our calculus analyzing the runtime of (a simplified version of) the BB84 quantum key distribution protocol.

arXiv:1911.11247•Nov 25, 2019•7 citations

On the Hardness of Analyzing Quantum Programs Quantitatively

Martin Avanzini, Georg Moser, Romain Péchoux +1 more

Abstract In this paper, we study quantitative properties of quantum programs. Properties of interest include (positive) almost-sure termination, expected runtime or expected cost, that is, for example, the expected number of applications of a given quantum gate, etc. After studying the completeness of these problems in the arithmetical hierarchy over the Clifford+T fragment of quantum mechanics, we express these problems using a variation of a quantum pre-expectation transformer, a weakest pre-condition based technique that allows to symbolically compute these quantitative properties. Under a smooth restriction—a restriction to polynomials of bounded degree over a real closed field—we show that the quantitative problem, which consists in finding an upper-bound to the pre-expectation, can be decided in time double-exponential in the size of a program, thus providing, despite its great complexity, one of the first decidable results on the analysis and verification of quantum programs. Finally, we sketch how the latter can be transformed into an efficient synthesis method.

arXiv:2312.13657•Lecture notes in computer science•Jan 1, 2024•2 citations
We study expected runtimes for quantum programs. Inspired by recent work on probabilistic programs, we first define expected runtime as a generalisation of quantum weakest precondition. Then, we show that the expected runtime of a quantum program can be represented as the expectation of an observable (in physics). A method for computing the expected runtimes of quantum programs in finite-dimensional state spaces is developed. Several examples are provided as applications of this method, including computing the expected runtime of quantum Bernoulli Factory -- a quantum algorithm for generating random numbers. In particular, using our new method, an open problem of computing the expected runtime of quantum random walks introduced by Ambainis et al. (STOC 2001) is solved.
We study expected runtimes for quantum programs. Inspired by recent work on probabilistic programs, we first define expected runtime as a generalisation of quantum weakest precondition. Then, we show that the expected runtime of a quantum program can be represented as the expectation of an observable (in physics). A method for computing the expected runtimes of quantum programs in finite-dimensional state spaces is developed. Several examples are provided as applications of this method, including computing the expected runtime of quantum Bernoulli Factory – a quantum algorithm for generating random numbers. In particular, using our new method, an open problem of computing the expected runtime of quantum random walks introduced by Ambainis et al. (STOC 2001) is solved.
We study expected runtimes for quantum programs. Inspired by recent work on probabilistic programs, we first define expected runtime as a generalisation of quantum weakest precondition . Then, we show that the expected runtime of a quantum program should be represented as the expectation of an observable (in physics). A method for computing the expected runtimes of quantum programs in finite-dimensional state spaces is developed. Several examples are provided as applications of this method, including computing the expected runtime of quantum Bernoulli Factory – a quantum algorithm for generating random numbers. In particular, using our new method, an open problem of computing the expected runtime of quantum random walks introduced by Ambainis et al. ( STOC 2001) is solved.
Quantum weakest preconditions are a fundamental tool for program verification of quantum programs. Many variations have been reported in the literature. We revisit quantum weakest preconditions from the perspective of expected runtime analysis of quantum programs and introduce a novel pre-expectation framework that enables to reason about the preconditions of quantum programs without the need of an upper bound. This is particularly interesting for quantum programs involving reward statements. The overall goal is to analyze runtime behavior even in the case of programs with potentially infinite expected runtime. This paper presents several ways to do so, e.g., a program transformation such that the expected runtime of a quantum program can be expressed using the weakest pre-expectation calculus with rewards.
Building upon recent work on probabilistic programs, we formally define the notion of expected runtime for quantum programs. A representation of the expected runtimes of quantum programs is introduced with an interpretation as an observable in physics. A method for computing the expected runtimes of quantum programs in finite-dimensional state spaces is developed. Several examples are provided as applications of this method; in particular, an open problem of computing the expected runtime of quantum random walks is solved using our method.
In this abstract we study the resource consumption of quantum programs. Specifically, we focus on the expected runtime of programs and, inspired by recent methods for probabilistic programs, we develop a calculus à la weakest precondition to formally and systematically derive the (exact) expected runtime of quantum programs. Notably, the calculus admits a notion of loop runtime invariant that can be readily used to derive upper bounds of their runtime. Finally, we show the applicability of our calculus analyzing the runtime of (a simplified version of) the BB84 quantum key distribution protocol.
Abstract In this paper, we study quantitative properties of quantum programs. Properties of interest include (positive) almost-sure termination, expected runtime or expected cost, that is, for example, the expected number of applications of a given quantum gate, etc. After studying the completeness of these problems in the arithmetical hierarchy over the Clifford+T fragment of quantum mechanics, we express these problems using a variation of a quantum pre-expectation transformer, a weakest pre-condition based technique that allows to symbolically compute these quantitative properties. Under a smooth restriction—a restriction to polynomials of bounded degree over a real closed field—we show that the quantitative problem, which consists in finding an upper-bound to the pre-expectation, can be decided in time double-exponential in the size of a program, thus providing, despite its great complexity, one of the first decidable results on the analysis and verification of quantum programs. Finally, we sketch how the latter can be transformed into an efficient synthesis method.