Model Checking Quantum Continuous-Time Markov Chains

Xu, M; Mei, J; Guan, J; Yu, N

Model Checking Quantum Continuous-Time Markov Chains

Xu, M Mei, J Guan, J Yu, N

Permalink

Publication Type:: Conference Proceeding
Citation:: Leibniz International Proceedings in Informatics, LIPIcs, 2021, 203
Issue Date:: 2021-08-01

Open Access

Copyright Clearance Process

Recently Added
In Progress
Open Access

This item is open access.

Adobe PDF

Download Published versionAdobe PDF (970.05 kB)

View on publisher's site

View statistics

Full metadata record

Field	Value	Language
dc.contributor.author	Xu, M
dc.contributor.author	Mei, J
dc.contributor.author	Guan, J
dc.contributor.author	Yu, N https://orcid.org/0000-0003-1188-3032
dc.date.accessioned	2022-03-31T03:59:09Z
dc.date.available	2022-03-31T03:59:09Z
dc.date.issued	2021-08-01
dc.identifier.citation	Leibniz International Proceedings in Informatics, LIPIcs, 2021, 203
dc.identifier.isbn	9783959772037
dc.identifier.issn	1868-8969
dc.identifier.uri	http://hdl.handle.net/10453/155765
dc.description.abstract	Verifying quantum systems has attracted a lot of interests in the last decades. In this paper, we initialise the model checking of quantum continuous-time Markov chain (QCTMC). As a real-time system, we specify the temporal properties on QCTMC by signal temporal logic (STL). To effectively check the atomic propositions in STL, we develop a state-of-the-art real root isolation algorithm under Schanuel's conjecture; further, we check the general STL formula by interval operations with a bottom-up fashion, whose query complexity turns out to be linear in the size of the input formula by calling the real root isolation algorithm. A running example of an open quantum walk is provided to demonstrate our method.
dc.language	en
dc.relation	http://purl.org/au-research/grants/arc/DE180100156
dc.relation	http://purl.org/au-research/grants/arc/DP210102449
dc.relation.ispartof	Leibniz International Proceedings in Informatics, LIPIcs
dc.relation.isbasedon	10.4230/LIPIcs.CONCUR.2021.13
dc.rights	info:eu-repo/semantics/openAccess
dc.title	Model Checking Quantum Continuous-Time Markov Chains
dc.type	Conference Proceeding
utslib.citation.volume	203
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	open_access	*
dc.date.updated	2022-03-31T03:59:08Z
pubs.publication-status	Published
pubs.volume	203

Abstract:

Verifying quantum systems has attracted a lot of interests in the last decades. In this paper, we initialise the model checking of quantum continuous-time Markov chain (QCTMC). As a real-time system, we specify the temporal properties on QCTMC by signal temporal logic (STL). To effectively check the atomic propositions in STL, we develop a state-of-the-art real root isolation algorithm under Schanuel's conjecture; further, we check the general STL formula by interval operations with a bottom-up fashion, whose query complexity turns out to be linear in the size of the input formula by calling the real root isolation algorithm. A running example of an open quantum walk is provided to demonstrate our method.

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

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