Qantum Weakest Preconditions for Reasoning about Expected Runtimes of Qantum Programs

Liu, J; Zhou, L; Barthe, G; Ying, M

Qantum Weakest Preconditions for Reasoning about Expected Runtimes of Qantum Programs

Liu, J Zhou, L Barthe, G Ying, M

Permalink

Publisher:: Association for Computing Machinery (ACM)
Publication Type:: Conference Proceeding
Citation:: Proceedings - Symposium on Logic in Computer Science, 2022, pp. 1-13
Issue Date:: 2022-08-02

Closed Access

	Filename	Description	Size
	Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs.pdf	Published version	715.32 kB	Adobe PDF	View/Open

Copyright Clearance Process

Recently Added
In Progress
Closed Access

This item is closed access and not available.

Full metadata record

Field	Value	Language
dc.contributor.author	Liu, J
dc.contributor.author	Zhou, L
dc.contributor.author	Barthe, G
dc.contributor.author	Ying, M https://orcid.org/0000-0003-4847-702X
dc.date.accessioned	2023-03-14T02:27:33Z
dc.date.available	2023-03-14T02:27:33Z
dc.date.issued	2022-08-02
dc.identifier.citation	Proceedings - Symposium on Logic in Computer Science, 2022, pp. 1-13
dc.identifier.isbn	9781450393515
dc.identifier.issn	1043-6871
dc.identifier.uri	http://hdl.handle.net/10453/167294
dc.description.abstract	We study expected runtimes for quantum programs. Inspired by recent work on probabilistic programs, we frst defne 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 fnite-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.
dc.language	en
dc.publisher	Association for Computing Machinery (ACM)
dc.relation	National Natural Science Foundation of China61832015
dc.relation.ispartof	Proceedings - Symposium on Logic in Computer Science
dc.relation.ispartof	Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science
dc.relation.isbasedon	10.1145/3531130.3533327
dc.rights	info:eu-repo/semantics/closedAccess
dc.title	Qantum Weakest Preconditions for Reasoning about Expected Runtimes of Qantum Programs
dc.type	Conference Proceeding
pubs.organisational-group	/University of Technology Sydney
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology
pubs.organisational-group	/University of Technology Sydney/Strength - QSI - Centre for Quantum Software and Information
utslib.copyright.status	closed_access	*
dc.date.updated	2023-03-14T02:27:32Z
pubs.publication-status	Published

Abstract:

We study expected runtimes for quantum programs. Inspired by recent work on probabilistic programs, we frst defne 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 fnite-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.

Please use this identifier to cite or link to this item:

http://hdl.handle.net/10453/167294