Verification of quantum programs

Ying, M; Yu, N; Feng, Y; Duan, R

Verification of quantum programs

Ying, M

Yu, N

Feng, Y

Duan, R

Permalink

Publication Type:: Journal Article
Citation:: Science of Computer Programming, 2013, 78 (9), pp. 1679 - 1700
Issue Date:: 2013-09-01

Closed Access

	Filename	Description	Size
	2012006187OK.pdf	Published Version	497.29 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	Ying, M https://orcid.org/0000-0003-4847-702X	en_US
dc.contributor.author	Yu, N https://orcid.org/0000-0003-1188-3032	en_US
dc.contributor.author	Feng, Y https://orcid.org/0000-0002-3097-3896	en_US
dc.contributor.author	Duan, R https://orcid.org/0000-0002-4388-7487	en_US
dc.date.issued	2013-09-01	en_US
dc.identifier.citation	Science of Computer Programming, 2013, 78 (9), pp. 1679 - 1700	en_US
dc.identifier.issn	0167-6423	en_US
dc.identifier.uri	http://hdl.handle.net/10453/32174
dc.description.abstract	This paper develops verification methodology for quantum programs, and the contribution of the paper is two-fold. Sharir, Pnueli and Hart [M. Sharir, A. Pnueli, S. Hart, Verification of probabilistic programs, SIAM Journal of Computing 13 (1984) 292-314] presented a general method for proving properties of probabilistic programs, in which a probabilistic program is modeled by a Markov chain and an assertion on the output distribution is extended to an invariant assertion on all intermediate distributions. Their method is essentially a probabilistic generalization of the classical Floyd inductive assertion method. In this paper, we consider quantum programs modeled by quantum Markov chains which are defined by super-operators. It is shown that the Sharir-Pnueli-Hart method can be elegantly generalized to quantum programs by exploiting the Schrödinger-Heisenberg duality between quantum states and observables. In particular, a completeness theorem for the Sharir-Pnueli-Hart verification method of quantum programs is established.As indicated by the completeness theorem, the Sharir-Pnueli-Hart method is in principle effective for verifying all properties of quantum programs that can be expressed in terms of Hermitian operators (observables). But it is not feasible for many practical applications because of the complicated calculation involved in the verification. For the case of finite-dimensional state spaces, we find a method for verification of quantum programs much simpler than the Sharir-Pnueli-Hart method by employing the matrix representation of super-operators and Jordan decomposition of matrices. In particular, this method enables us to compute easily the average running time and to analyze some interesting long-run behaviors of quantum programs in a finite-dimensional state space. © 2012 Elsevier B.V. All rights reserved.	en_US
dc.relation.ispartof	Science of Computer Programming	en_US
dc.relation.isbasedon	10.1016/j.scico.2013.03.016	en_US
dc.subject.classification	Software Engineering	en_US
dc.title	Verification of quantum programs	en_US
dc.type	Journal Article
utslib.citation.volume	9	en_US
utslib.citation.volume	78	en_US
utslib.for	0802 Computation Theory and Mathematics	en_US
utslib.for	0803 Computer Software	en_US
pubs.embargo.period	Not known	en_US
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
pubs.issue	9	en_US
pubs.publication-status	Published	en_US
pubs.volume	78	en_US

Abstract:

This paper develops verification methodology for quantum programs, and the contribution of the paper is two-fold. Sharir, Pnueli and Hart [M. Sharir, A. Pnueli, S. Hart, Verification of probabilistic programs, SIAM Journal of Computing 13 (1984) 292-314] presented a general method for proving properties of probabilistic programs, in which a probabilistic program is modeled by a Markov chain and an assertion on the output distribution is extended to an invariant assertion on all intermediate distributions. Their method is essentially a probabilistic generalization of the classical Floyd inductive assertion method. In this paper, we consider quantum programs modeled by quantum Markov chains which are defined by super-operators. It is shown that the Sharir-Pnueli-Hart method can be elegantly generalized to quantum programs by exploiting the Schrödinger-Heisenberg duality between quantum states and observables. In particular, a completeness theorem for the Sharir-Pnueli-Hart verification method of quantum programs is established.As indicated by the completeness theorem, the Sharir-Pnueli-Hart method is in principle effective for verifying all properties of quantum programs that can be expressed in terms of Hermitian operators (observables). But it is not feasible for many practical applications because of the complicated calculation involved in the verification. For the case of finite-dimensional state spaces, we find a method for verification of quantum programs much simpler than the Sharir-Pnueli-Hart method by employing the matrix representation of super-operators and Jordan decomposition of matrices. In particular, this method enables us to compute easily the average running time and to analyze some interesting long-run behaviors of quantum programs in a finite-dimensional state space. © 2012 Elsevier B.V. All rights reserved.

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

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