  Verifying quantum systems has attracted a lot of interests in the last
decades. In this paper, we initialised 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-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.
