Symbolic bisimulation for quantum processes

Feng, Y; Deng, Y; Ying, M

Symbolic bisimulation for quantum processes

Feng, Y

Deng, Y Ying, M

Permalink

Publication Type:: Journal Article
Citation:: ACM Transactions on Computational Logic, 2014, 15 (2)
Issue Date:: 2014-01-01

Closed Access

	Filename	Description	Size
	qsb.pdf		845.2 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	en_US
dc.contributor.author	Deng, Y	en_US
dc.contributor.author	Ying, M https://orcid.org/0000-0003-4847-702X	en_US
dc.date.issued	2014-01-01	en_US
dc.identifier.citation	ACM Transactions on Computational Logic, 2014, 15 (2)	en_US
dc.identifier.issn	1529-3785	en_US
dc.identifier.uri	http://hdl.handle.net/10453/33134
dc.identifier.uri	http://hdl.handle.net/10453/33288
dc.identifier.uri	http://hdl.handle.net/10453/33287
dc.identifier.uri	http://hdl.handle.net/10453/33135
dc.identifier.uri	http://hdl.handle.net/10453/33133
dc.identifier.uri	http://hdl.handle.net/10453/33002
dc.description.abstract	With the previous notions of bisimulation presented in the literature, to check if two quantum processes are bisimilar, we have to instantiate their free quantum variables with arbitrary quantum states, and verify the bisimilarity of the resulting configurations. This makes checking bisimilarity infeasible from an algorithmic point of view, because quantum states constitute a continuum. In this article, we introduce a symbolic operational semantics for quantum processes directly at the quantum operation level, which allows us to describe the bisimulation between quantum processes without resorting to quantum states. We show that the symbolic bisimulation defined here is equivalent to the open bisimulation for quantum processes in previous work, when strong bisimulations are considered. An algorithm for checking symbolic ground bisimilarity is presented. We also give a modal characterisation for quantum bisimilarity based on an extension of Hennessy-Milner logic to quantum processes. © 2014 ACM.	en_US
dc.relation.ispartof	ACM Transactions on Computational Logic	en_US
dc.relation.isbasedon	10.1145/2579818	en_US
dc.subject.classification	Computation Theory & Mathematics	en_US
dc.title	Symbolic bisimulation for quantum processes	en_US
dc.type	Journal Article
utslib.citation.volume	2	en_US
utslib.citation.volume	15	en_US
utslib.for	080203 Computational Logic and Formal Languages	en_US
utslib.for	0101 Pure Mathematics	en_US
utslib.for	0801 Artificial Intelligence and Image Processing	en_US
utslib.for	0802 Computation Theory and Mathematics	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	2	en_US
pubs.publication-status	Published	en_US
pubs.volume	15	en_US

Abstract:

With the previous notions of bisimulation presented in the literature, to check if two quantum processes are bisimilar, we have to instantiate their free quantum variables with arbitrary quantum states, and verify the bisimilarity of the resulting configurations. This makes checking bisimilarity infeasible from an algorithmic point of view, because quantum states constitute a continuum. In this article, we introduce a symbolic operational semantics for quantum processes directly at the quantum operation level, which allows us to describe the bisimulation between quantum processes without resorting to quantum states. We show that the symbolic bisimulation defined here is equivalent to the open bisimulation for quantum processes in previous work, when strong bisimulations are considered. An algorithm for checking symbolic ground bisimilarity is presented. We also give a modal characterisation for quantum bisimilarity based on an extension of Hennessy-Milner logic to quantum processes. © 2014 ACM.

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

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