Model-checking linear-time properties of quantum systems

Ying, M; Li, Y; Yu, N; Feng, Y

Model-checking linear-time properties of quantum systems

Ying, M

Li, Y Yu, N

Feng, Y

Permalink

Publication Type:: Journal Article
Citation:: ACM Transactions on Computational Logic, 2014, 15 (3)
Issue Date:: 2014-07-08

Closed Access

	Filename	Description	Size
	2014 Model-Checking Linear-Time Properties of Quantum Systems.pdf	Published Version	359.19 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	Li, Y	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.date.issued	2014-07-08	en_US
dc.identifier.citation	ACM Transactions on Computational Logic, 2014, 15 (3)	en_US
dc.identifier.issn	1529-3785	en_US
dc.identifier.uri	http://hdl.handle.net/10453/34576
dc.description.abstract	© 2014 ACM. We define a formal framework for reasoning about linear-time properties of quantum systems in which quantum automata are employed in the modeling of systems and certain (closed) subspaces of state Hilbert spaces are used as the atomic propositions about the behavior of systems. We provide an algorithm for verifying invariants of quantum automata. Then, an automata-based model-checking technique is generalized for the verification of safety properties recognizable by reversible automata and ω?properties recognizable by reversible Büchi automata.	en_US
dc.relation	http://purl.org/au-research/grants/arc/DP130102764
dc.relation	http://purl.org/au-research/grants/arc/DP110103473
dc.relation.ispartof	ACM Transactions on Computational Logic	en_US
dc.relation.isbasedon	10.1145/2629680	en_US
dc.subject.classification	Computation Theory & Mathematics	en_US
dc.title	Model-checking linear-time properties of quantum systems	en_US
dc.type	Journal Article
utslib.citation.volume	3	en_US
utslib.citation.volume	15	en_US
utslib.for	0802 Computation Theory and Mathematics	en_US
utslib.for	0101 Pure Mathematics	en_US
utslib.for	0801 Artificial Intelligence and Image Processing	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	3	en_US
pubs.publication-status	Published	en_US
pubs.volume	15	en_US

Abstract:

© 2014 ACM. We define a formal framework for reasoning about linear-time properties of quantum systems in which quantum automata are employed in the modeling of systems and certain (closed) subspaces of state Hilbert spaces are used as the atomic propositions about the behavior of systems. We provide an algorithm for verifying invariants of quantum automata. Then, an automata-based model-checking technique is generalized for the verification of safety properties recognizable by reversible automata and ω?properties recognizable by reversible Büchi automata.

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

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