Verification of Distributed Quantum Programs

Feng, Y; Li, S; Ying, M

Verification of Distributed Quantum Programs

Feng, Y

Li, S Ying, M

Permalink

Publisher:: Association for Computing Machinery (ACM)
Publication Type:: Journal Article
Citation:: ACM Transactions on Computational Logic, 2022, abs/2104.14796
Issue Date:: 2022-03-29

Closed Access

	Filename	Description	Size
	3517145.pdf	Published version	594.77 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	Feng, Y https://orcid.org/0000-0002-3097-3896
dc.contributor.author	Li, S
dc.contributor.author	Ying, M
dc.date.accessioned	2022-04-12T22:09:20Z
dc.date.available	2022-04-12T22:09:20Z
dc.date.issued	2022-03-29
dc.identifier.citation	ACM Transactions on Computational Logic, 2022, abs/2104.14796
dc.identifier.issn	1529-3785
dc.identifier.issn	1557-945X
dc.identifier.uri	http://hdl.handle.net/10453/156147
dc.description.abstract	<jats:p>Distributed quantum systems and especially the Quantum Internet have the ever-increasing potential to fully demonstrate the power of quantum computation. This is particularly true given that developing a general-purpose quantum computer is much more difficult than connecting many small quantum devices. One major challenge of implementing distributed quantum systems is programming them and verifying their correctness. In this paper, we propose a CSP-like distributed programming language to facilitate the specification and verification of such systems. After presenting its operational and denotational semantics, we develop a Hoare-style logic for distributed quantum programs and establish its soundness and (relative) completeness with respect to both partial and total correctness. The effectiveness of the logic is demonstrated by its applications in the verification of quantum teleportation and local implementation of non-local CNOT gates, two important algorithms widely used in distributed quantum systems.</jats:p>
dc.language	en
dc.publisher	Association for Computing Machinery (ACM)
dc.relation.ispartof	ACM Transactions on Computational Logic
dc.relation.isbasedon	10.1145/3517145
dc.rights	info:eu-repo/semantics/closedAccess
dc.subject	0101 Pure Mathematics, 0801 Artificial Intelligence and Image Processing, 0802 Computation Theory and Mathematics
dc.subject.classification	Computation Theory & Mathematics
dc.title	Verification of Distributed Quantum Programs
dc.type	Journal Article
utslib.citation.volume	abs/2104.14796
utslib.for	0101 Pure Mathematics
utslib.for	0801 Artificial Intelligence and Image Processing
utslib.for	0802 Computation Theory and Mathematics
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	2022-04-12T22:09:19Z
pubs.publication-status	Published online
pubs.volume	abs/2104.14796

Abstract:

Distributed quantum systems and especially the Quantum Internet have the ever-increasing potential to fully demonstrate the power of quantum computation. This is particularly true given that developing a general-purpose quantum computer is much more difficult than connecting many small quantum devices. One major challenge of implementing distributed quantum systems is programming them and verifying their correctness. In this paper, we propose a CSP-like distributed programming language to facilitate the specification and verification of such systems. After presenting its operational and denotational semantics, we develop a Hoare-style logic for distributed quantum programs and establish its soundness and (relative) completeness with respect to both partial and total correctness. The effectiveness of the logic is demonstrated by its applications in the verification of quantum teleportation and local implementation of non-local CNOT gates, two important algorithms widely used in distributed quantum systems.

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

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