@inproceedings{18f0160a9baa4a9b988a40ddcf3d909c,
title = "Model Checking Quantum Continuous-Time Markov Chains",
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.",
keywords = "Computer algebra, Formal logic, Model checking, Quantum computing",
author = "Ming Xu and Jingyi Mei and Ji Guan and Nengkun Yu",
note = "Publisher Copyright: {\textcopyright} Ming Xu, Jingyi Mei, Ji Guan, and Nengkun Yu;.; 32nd International Conference on Concurrency Theory, CONCUR 2021 ; Conference date: 24-08-2021 Through 27-08-2021",
year = "2021",
month = aug,
day = "1",
doi = "10.4230/LIPIcs.CONCUR.2021.13",
language = "English",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
editor = "Serge Haddad and Daniele Varacca",
booktitle = "32nd International Conference on Concurrency Theory, CONCUR 2021",
}