2026-07-23T17:37:42Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:14390 2024-03-06T10:54:17Z ddc:004 open_access

Model Checking Quantum Continuous-Time Markov Chains Xu, Ming Mei, Jingyi Guan, Ji Yu, Nengkun Model Checking Formal Logic Quantum Computing Computer Algebra 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Ming Xu and Jingyi Mei and Ji Guan and Nengkun Yu 2021 Is Part Of LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2021.13 urn:nbn:de:0030-drops-143908 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.13 eng https://creativecommons.org/licenses/by/4.0/legalcode