| Field |
Value |
Language |
|
dc.contributor.author |
Guan, J |
|
|
dc.contributor.author |
Feng, Y |
|
|
dc.contributor.author |
Turrini, A |
|
|
dc.contributor.author |
Ying, M
https://orcid.org/0000-0003-4847-702X
|
|
|
dc.date.accessioned |
2024-09-02T05:00:53Z |
|
|
dc.date.available |
2024-09-02T05:00:53Z |
|
|
dc.date.issued |
2024 |
|
|
dc.identifier.citation |
Lecture Notes in Computer Science, 2024, 14683, pp. 533-554 |
|
|
dc.identifier.isbn |
9783031656323 |
|
|
dc.identifier.issn |
1611-3349 |
|
|
dc.identifier.issn |
1611-3349 |
|
|
dc.identifier.uri |
http://hdl.handle.net/10453/180589
|
|
|
dc.description.abstract |
<jats:title>Abstract</jats:title><jats:p>Model-checking techniques have been extended to analyze quantum programs and communication protocols represented as quantum Markov chains, an extension of classical Markov chains. To specify qualitative temporal properties, a subspace-based quantum temporal logic is used, which is built on Birkhoff-von Neumann atomic propositions. These propositions determine whether a quantum state is within a subspace of the entire state space. In this paper, we propose the measurement-based linear-time temporal logic MLTL to check quantitative properties. MLTL builds upon classical linear-time temporal logic (LTL) but introduces quantum atomic propositions that reason about the probability distribution after measuring a quantum state. To facilitate verification, we extend the symbolic dynamics-based techniques for stochastic matrices described by Agrawal et al. (JACM 2015) to handle more general quantum linear operators (super-operators) through eigenvalue analysis. This extension enables the development of an efficient algorithm for approximately model checking a quantum Markov chain against an MLTL formula. To demonstrate the utility of our model-checking algorithm, we use it to simultaneously verify linear-time properties of both quantum and classical random walks. Through this verification, we confirm the previously established advantages discovered by Ambainis et al. (STOC 2001) of quantum walks over classical random walks and discover new phenomena unique to quantum walks.</jats:p> |
|
|
dc.language |
en |
|
|
dc.publisher |
Springer Nature |
|
|
dc.relation |
http://purl.org/au-research/grants/arc/DP220102059
|
|
|
dc.relation.ispartof |
Lecture Notes in Computer Science |
|
|
dc.relation.ispartofseries |
Lecture Notes in Computer Science |
|
|
dc.relation.isbasedon |
10.1007/978-3-031-65633-0_24 |
|
|
dc.rights |
info:eu-repo/semantics/openAccess |
|
|
dc.subject.classification |
Artificial Intelligence & Image Processing |
|
|
dc.subject.classification |
46 Information and computing sciences |
|
|
dc.title |
Measurement-Based Verification of Quantum Markov Chains |
|
|
dc.type |
Conference Proceeding |
|
|
utslib.citation.volume |
14683 |
|
|
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 |
|
|
pubs.organisational-group |
University of Technology Sydney/Faculty of Engineering and Information Technology/School of Computer Science |
|
|
pubs.organisational-group |
University of Technology Sydney/Strength - CQSI - Centre for Quantum Software and Information |
|
|
pubs.organisational-group |
University of Technology Sydney/All Manual Groups |
|
|
pubs.organisational-group |
University of Technology Sydney/All Manual Groups/Centre for Quantum Software and Information (QSI) |
|
|
utslib.copyright.status |
open_access |
* |
|
dc.rights.license |
This work is licensed under a Creative Commons Attribution 4.0 International License (CC BY 4.0). To view a copy of this license, visit https://creativecommons.org/licenses/by/4.0/ |
|
|
dc.date.updated |
2024-09-02T05:00:51Z |
|
|
pubs.publication-status |
Published |
|
|
pubs.volume |
14683 |
|
