Shanghai Key Lab of Trustworthy Computing, East China Normal University,
<EMAIL_ADDRESS>Shanghai Key Lab of Trustworthy Computing, East China
Normal University<EMAIL_ADDRESS>State Key Lab of Computer Science,
Institute of Software, Chinese Academy of Sciences<EMAIL_ADDRESS>Centre for Quantum Software and Information, University of Technology Sydney,
<EMAIL_ADDRESS>TBD [500]Theory of computation Verification by
model checking [500]Computing methodologies Symbolic and algebraic algorithms
[300]Theory of computation Quantum computation theory John Q. Open and Joan R.
Access 2 42nd Conference on Very Important Topics (CVIT 2016) CVIT 2016
December 24–27, 2016 Little Whinging, United Kingdom 42 23

# Model Checking Quantum Continuous-Time Markov Chains

Ming Xu  Jingyi Mei  Ji Guan  Nengkun Yu

###### Abstract

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.

###### keywords:

Model Checking, Formal Logic, Quantum Computing, Computer Algebra

##  1 Introduction

Aiming to study nature, physicists use different mechanics depending on the
scale of the objects they are interested in. Classical mechanics describes
nature at macroscopic scale (far larger than $10^{-9}$ meters), while quantum
mechanics is applied at microscopic scale (near or less than $10^{-9}$
meters). A particle at this level can be mathematically represented by a
normalised complex vector $\ket{s}$ in a Hilbert space $\mathcal{H}$. The time
evolution of a single particle _closed_ system is described by the Schrödinger
equation

$\frac{\mathrm{d}\ket{s(t)}}{\mathrm{d}t}=-\imath\mathbf{H}\ket{s(t)}$ (1)

with some _Hamiltonian_ $\mathbf{H}$ (a Hermitian matrix on $\mathcal{H}$),
where $\ket{s(t)}$ is the state of the system at time $t$. More practically,
an _open_ quantum system interacting with the surrounding environment need to
be considered. Suffering noises from the environment, the state of the system
cannot be completely known. Thus a _density operator_ $\rho$ (positive
semidefinite matrix with unit trace) on $\mathcal{H}$ is introduced to
describe the uncertainty of the possible states: $\rho=\sum_{i\in
I}p_{i}\op{s_{i}}{s_{i}}$, where $\\{(p_{i},\ket{s_{i}})\\}_{i\in I}$ is a
mixed state or an ensemble expressing that the quantum state is at
$\ket{s_{i}}$ with probability $p_{i}$, and $\bra{s_{i}}$ is the complex
conjugate and transpose of $\ket{s_{i}}$. In this case, the evolution is
described by the Lindblad’s master equation:

$\frac{\mathrm{d}\rho(t)}{\mathrm{d}t}=\mathcal{L}(\rho(t))$ (2)

where $\rho(t)$ stands for the (possibly mixed) state of the system, and
$\mathcal{L}$ is a linear function of $\rho(t)$ (to be formally described in
Subsection 2.2), which is generally irreversible.

To reveal physical phenomenon, physicists have intensively studied the
properties of closed and open quantum systems case by case in the last
decades, such as long-term behaviors (e.g. [18]) and stabilities (e.g. [10]).
In recent years, the computer science community has stepped into this field
and adopted model checking technique to study quantum systems [16, 17].
Specifically, the quantum systems can be simulated by some mathematical models
and a bulk of physical properties can be reformulated as formulas in some
temporal logic with atomic propositions of quantum interpretation. In
particular, a _quantum discrete-time Markov chain_ (QDTMC)
$(\mathcal{H},\mathcal{E})$ has been introduced as quantum generalisations of
classical discrete-time Markov chains (DTMC) to model the evolution in Eq. (2)
in a single time unit:

$\rho(t+1)=\mathcal{E}(\rho(t))$ (3)

where $\mathcal{E}$ is a discretised quantum operation obtained from the
Lindblad’s master equation, usually called a _super-operator_ in the field of
quantum information and computation. Several fundamental model checking-
related problems for QDTMCs have been studied in the literature, including
limiting states [40, 21], reachability [45, 41], repeated reachability [14],
linear time properties [30], and persistence based on irreducible and periodic
decomposition techniques [8, 21]. These techniques were equipped to solve
real-world problems in several different areas. For example, [15] proposed
algorithms to model checking quantum cryptographic protocols against a quantum
extension of probabilistic computation tree logic (PCTL); and linear temporal
logic (LTL) was adopted to specify a bulk of properties of quantum many-body
and statistical systems, and corresponding model checking algorithm was
developed [20]. See [43, 44] for the comprehensive review of this research
line.

However, to the best of our knowledge, there is no work on model checking the
quantum continuous-time system of Eq. (2). In contrast, there are fruitful
results in the classical counterpart, which is usually modelled by a
continuous-time Markov chain (CTMC).

The seminal work on verifying CTMCs is Aziz et al.’s paper [3, 4]. The authors
introduced continuous stochastic logic (CSL) interpreted on CTMCs. Roughly
speaking, the syntax of CSL amounts to that of PCTL plus the multiphase until
formula
$\Phi_{1}\mathrm{U}\,^{\mathcal{I}_{1}}\Phi_{2}\cdots\mathrm{U}\,^{\mathcal{I}_{K}}\Phi_{K+1}$,
for some $K\geq 1$. Because [3] restricts probabilities in $\Pr_{>\texttt{c}}$
to $\texttt{c}\in\mathbb{Q}$, they can show decidability of model checking for
CSL using number-theoretic analysis. An approximate model checking algorithm
for a reduced version of CSL was provided by Baier et al. [6], who restrict
path formulas to binary until: $\Phi_{1}\mathrm{U}\,^{\mathcal{I}}\Phi_{2}$.
Under this logic, they successfully applied efficient numerical techniques for
_transient analysis_ [5] using _uniformisation_ [37]. The approximate
algorithms have been extended for multiphase until formulas using
_stratification_ [46, 47]. Xu et al. considered the multi-phase until formulas
over the CTMC with rewards [42]. An integral-style algorithm was proposed to
attack this problem, whose effectiveness is ensured by number-theoretic
results and algebraic methods. Recently, continuous linear logic was
introduced to specified on CTMCS, whose decidability was established [23].
Most the above algorithms have been implemented in probabilistic model
checkers, like PRISM [29], Storm [13], and ePMC [24].

Unfortunately, these results from CTMCs cannot directly tackle the problem of
automatically verifying quantum continuous-time systems. The main obstacle is
that the state space of classical case is finite, while the space of quantum
states in even a finite-dimensional Hilbert space is continuum (i.e.,
infinite). In this paper, we cross the difficulty by introducing quantum
continuous-time Markov chains (QCTMC) to model the evolution of quantum
continuous-time systems in Eq. (2) and converting them into a distribution
transformer that preserves the laws of quantum mechanics. Then, we consider a
wide logic, signal temporal logic (STL), to specify real-time properties
against QCTMC. The STL is more expressible than LTL and CTL. Finally we
present an exact method to decide the STL formula using real root isolation
and interval operations, whose query complexity turns out to be linear in the
size of the input formula by calling the real root isolation routine.

The key contributions of the present paper are three-fold:

  1. 1.

In the field of formal verification, the model checking on DTMC, QDTMC and
CTMC has been well studied in the past decades, but no work on checking QCTMCs
as far as we know. The first contribution is filling this blank.

  2. 2.

In order to solve the atomic propositions in STL, we develop a state-of-the-
art real root isolation algorithm for a rich class of real-valued functions
based on Schanuel’s conjecture.

  3. 3.

We provide a running example—open quantum walk equipped with an absorbing
boundary, which drops the restriction on the underlying graph being
symmetric/Hermitian. The non-Hermitian structure brings real technical
hardness. Fortunately, it is overcome by Eq. (2) employed for describing the
dynamical system of QCTMC.

#### Organisation

The rest of the paper is structured as follows. Section 2 review some notions
and notations in quantum computing, the Lindblad’s master equation and number
theory. In Sections 3 and 4, we introduce the model of quantum continuous-time
Markov chains and the signal temporal logic (STL), respectively. We solve the
atomic propositions in STL in Section 5, and decide the general STL formulas
in Section 6. Section 7 is the conclusion.

##  2 Preliminaries

Here we will recall some useful notions and notations from quantum computing
[34], the Lindblad’s master equation and number theory.

###  2.1 Quantum Computing

Let $\mathcal{H}$ be a Hilbert space with dimension $d$. We employ the Dirac
notations that are standard in quantum computing:

  * •

$\ket{s}$ stands for a unit column vector in $\mathcal{H}$ labelled with $s$;

  * •

$\bra{s}:=\ket{s}^{\dagger}$ is the Hermitian adjoint (complex conjugate and
transpose) of $\ket{s}$;

  * •

$\ip{s_{1}}{s_{2}}:=\bra{s_{1}}\ket{s_{2}}$ is the inner product of
$\ket{s_{1}}$ and $\ket{s_{2}}$;

  * •

$\op{s_{1}}{s_{2}}:=\ket{s_{1}}\otimes\bra{s_{2}}$ is the outer product, where
$\otimes$ denotes tensor product; and

  * •

$\ket{s_{1},s_{2}}:=\ket{s_{1}}\ket{s_{2}}$ is a shorthand of the product
state $\ket{s_{1}}\otimes\ket{s_{2}}$.

A linear operator $\gamma$ is _Hermitian_ if $\gamma=\gamma^{\dagger}$; and it
is _positive_ if $\bra{s}\gamma\ket{s}\geq 0$ holds for any
$\ket{s}\in\mathcal{H}$. A _projector_ $\mathbf{P}$ is a positive operator of
the form $\sum_{i=1}^{m}\op{s_{i}}{s_{i}}$ with $m\leq d$, where $\ket{s_{i}}$
are orthonormal. Clearly, there is a bijective map between projectors
$\mathbf{P}=\sum_{i=1}^{m}\op{s_{i}}{s_{i}}$ and subspaces of $\mathcal{H}$
that are spanned by $\\{\ket{s_{i}}:1\leq i\leq m\\}$. In sum, positive
operators are Hermitian ones whose eigenvalues are nonnegative; and projectors
are positive operators whose eigenvalues are $0$ or $1$. Besides, a linear
operator $\mathbf{U}$ is _unitary_ if
$\mathbf{U}\mathbf{U}^{\dagger}=\mathbf{U}^{\dagger}\mathbf{U}=\mathbf{I}$
where $\mathbf{I}$ is the _identity_ operator.

The _trace_ of a linear operator $\gamma$ is defined as
$\mathrm{tr}(\gamma):=\sum_{i=1}^{d}\bra{s_{i}}\gamma\ket{s_{i}}$ for any
orthonormal basis $\\{\ket{s_{i}}:1\leq i\leq d\\}$ of $\mathcal{H}$. A
_density operator_ $\rho$ on $\mathcal{H}$ is a positive operator with unit
trace. It gives rise to a generic way to describe quantum states: if a density
operator $\rho$ is $\op{s}{s}$ for some $\ket{s}\in\mathcal{H}$, $\rho$ is
said to be a _pure_ state; otherwise it is a _mixed_ one, i.e.
$\rho=\sum_{i=1}^{m}p_{i}\op{s_{i}}{s_{i}}$ with $m\geq 2$ by spectral
decomposition, where $p_{i}$ are positive eigenvalues (interpreted as the
_probabilities_ of taking the pure states $\ket{s_{i}}$) and their sum is $1$.
In other words, a pure state indicates the system state which we completely
know; a mixed state gives all possible system states, with total probability
$1$, which we know. We denote by $\mathcal{D}_{\mathcal{H}}$ the set of
density operators on $\mathcal{H}$. The subscript $\mathcal{H}$ of
$\mathcal{D}_{\mathcal{H}}$ will be omitted if it is clear from the context.

The system evolution between pure states is characterised by some unitary
operator $\mathbf{U}$, i.e.
$\op{s(t)}{s(t)}=\mathbf{U}(t)\op{s(0)}{s(0)}\mathbf{U}^{\dagger}(t)$ where
$\mathbf{U}(t)$ comes from $\exp(-\imath\mathbf{H}t)$ for the Hermitian
operator $\mathbf{H}$ in Eq. (1); the system evolution between density
operators (pure or mixed states) is characterised by some completely positive
operator-sum, a.k.a. _super-operator_ , i.e.
$\rho(t)=\sum_{j=1}^{m}\mathbf{L}_{j}(t)\rho(0)\mathbf{L}_{j}^{\dagger}(t)$
where $\mathbf{L}_{j}$ are linear operators satisfying the trace preservation
$\sum_{j=1}^{m}\mathbf{L}_{j}^{\dagger}\mathbf{L}_{j}=\mathbf{I}$. The latter
dynamical system is obtained in such a way: an enlarged unitary operator acts
on the purified composite state
$(\sum_{i=1}^{m}\sqrt{p_{i}}\ket{s_{i},env_{i}})(\sum_{i=1}^{m}\sqrt{p_{i}}\bra{s_{i},env_{i}})$
with $\rho(0)=\sum_{i=1}^{m}p_{i}\op{s_{i}}{s_{i}}$ for some orthonormal
environment states $\ket{env_{i}}$ [34, Section 2.5], then the environment in
the resulting composite state is traced out, which turns out to be the
aforementioned operator-sum form. We call it an _open_ system as it interacts
with the environment. Whereas, the former dynamical system, independent from
the environment, is called a _closed_ system. Open systems are more common
than closed systems in practice.

###  2.2 Lindblad’s Master Equation

To characterise state evolution of the continuous-time open system with the
_memoryless_ property, we employ the Lindblad’s master equation [31, 19] that
is

$\rho^{\prime}=\mathcal{L}(\rho)=-\imath\mathbf{H}\rho+\imath\rho\mathbf{H}+\sum_{j=1}^{m}\left(\mathbf{L}_{j}\rho\mathbf{L}_{j}^{\dagger}-\tfrac{1}{2}\mathbf{L}_{j}^{\dagger}\mathbf{L}_{j}\rho-\tfrac{1}{2}\rho\mathbf{L}_{j}^{\dagger}\mathbf{L}_{j}\right),$
(4)

where $\mathbf{H}$ is a Hermitian operator and $\mathbf{L}_{j}$ are linear
operators. The terms $-\imath\mathbf{H}\rho+\imath\rho\mathbf{H}$ describe the
evolution of the internal system; the terms
$\mathbf{L}_{j}\rho\mathbf{L}_{j}^{\dagger}-\tfrac{1}{2}\mathbf{L}_{j}^{\dagger}\mathbf{L}_{j}\rho-\tfrac{1}{2}\rho\mathbf{L}_{j}^{\dagger}\mathbf{L}_{j}$
describe the interaction between system and environment. In other words, to
characterise the evolution of an open system, it is necessary to use those
linear operators $\mathbf{L}_{j}$ besides the Hermitian operator $\mathbf{H}$.
It is known to be the most general type of Markovian and time-homogeneous
master equation describing (in general non-unitary) evolution of the system
state that preserves the laws of quantum mechanics (i.e., completely positive
and trace-preserving for any initial condition).

In the following, we will derive the solution of Eq. (4). We first define two
useful functions:

  * •

$\mathrm{L2V}(\gamma):=\sum_{i=1}^{d}\sum_{j=1}^{d}\bra{i}\gamma\ket{j}\ket{i,j}$
that rearranges entries of the linear operator $\gamma$ on the Hilbert space
$\mathcal{H}$ with dimension $d$ as a column vector; and

  * •

$\mathrm{V2L}(\mathbf{v}):=\sum_{i=1}^{d}\sum_{j=1}^{d}\bra{i,j}\mathbf{v}\op{i}{j}$
that rearranges entries of the column vector $\mathbf{v}$ as a linear
operator.

Here, $\mathrm{L2V}$ and $\mathrm{V2L}$ are read as “linear operator to
vector” and “vector to linear operator”, respectively. They are mutually
inverse functions, so that if a linear operator (resp. its vectorisation) is
determined, its vectorisation (resp. the original linear operator) is
determined. Using the fact that
$\mathbf{D}=\mathbf{A}\mathbf{B}\mathbf{C}\Longleftrightarrow\mathrm{L2V}(\mathbf{D})=(\mathbf{A}\otimes\mathbf{C}^{\mathrm{T}})\mathrm{L2V}(\mathbf{B})$
holds for any linear operators $\mathbf{A},\mathbf{B},\mathbf{C},\mathbf{D}$,
we can reformulate Eq. (4) as the linear ordinary differential equation

$\displaystyle\mathrm{L2V}(\rho^{\prime})$
$\displaystyle=\left[-\imath\mathbf{H}\otimes\mathbf{I}+\imath\mathbf{I}\otimes\mathbf{H}^{\mathrm{T}}+\sum_{j=1}^{m}\left(\mathbf{L}_{j}\otimes\mathbf{L}_{j}^{*}-\tfrac{1}{2}\mathbf{L}_{j}^{\dagger}\mathbf{L}_{j}\otimes\mathbf{I}-\tfrac{1}{2}\mathbf{I}\otimes\mathbf{L}_{j}^{\mathrm{T}}\mathbf{L}_{j}^{*}\right)\right]\mathrm{L2V}(\rho)$
(5) $\displaystyle=\mathds{M}\cdot\mathrm{L2V}(\rho),$

where $*$ denotes entry-wise complex conjugate. We call
$\mathds{M}=-\imath\mathbf{H}\otimes\mathbf{I}+\imath\mathbf{I}\otimes\mathbf{H}^{\mathrm{T}}+\sum_{j=1}^{m}\big{(}\mathbf{L}_{j}\otimes\mathbf{L}_{j}^{*}-\tfrac{1}{2}\mathbf{L}_{j}^{\dagger}\mathbf{L}_{j}\otimes\mathbf{I}\linebreak[0]-\tfrac{1}{2}\mathbf{I}\otimes\mathbf{L}_{j}^{\mathrm{T}}\mathbf{L}_{j}^{*}\big{)}$
the _governing matrix_ of Eq. (5). As a result, we get the desired solution
$\mathrm{L2V}(\rho(t))=\exp(\mathds{M}\cdot t)\cdot\mathrm{L2V}(\rho(0))$ or
equivalently $\rho(t)=\mathrm{V2L}(\exp(\mathds{M}\cdot
t)\cdot\mathrm{L2V}(\rho(0)))$ in a closed form. It can be obtained in
polynomial time by the standard method [27].

###  2.3 Number Theory

######  Definition 2.1.

A number $\alpha$ is _algebraic_ , denoted by $\alpha\in\mathbb{A}$, if there
is a nonzero $\mathbb{Q}$-polynomial $f_{\alpha}(z)$ of least degree,
satisfying $f_{\alpha}(\alpha)=0$; otherwise $\alpha$ is _transcendental_.

In the above definition, such a polynomial $f_{\alpha}(z)$ is called the
_minimal polynomial_ of $\alpha$. The _degree_ $D$ of $\alpha$ is
$\deg_{z}(f_{\alpha})$. The standard encoding of $\alpha$ is the minimal
polynomial $f_{\alpha}$ plus an isolation disk in the complex plane that
distinguishes $\alpha$ from other roots of $f_{\alpha}$.

######  Definition 2.2.

Let $\mu_{1},\ldots,\mu_{m}$ be irrational complex numbers. Then the _field
extension_ $\mathbb{Q}(\mu_{1},\ldots,\mu_{m}):\mathbb{Q}$ is the smallest set
that contains $\mu_{1},\ldots,\mu_{m}$ and is closed under arithmetic
operations, i.e. addition, substraction, multiplication and division.

Here those irrational complex numbers $\mu_{1},\ldots,\mu_{m}$ are called the
generators of the field extension. A field extension is _simple_ if it has
only one generator. For instance, the field extension
$\mathbb{Q}(\sqrt{2}):\mathbb{Q}$ is exactly the set
$\\{a+b\sqrt{2}:a,b\in\mathbb{Q}\\}$.

######  Lemma 2.3 ([32, Algorithm 2]).

Let $\alpha_{1}$ and $\alpha_{2}$ be two algebraic numbers of degrees $D_{1}$
and $D_{2}$, respectively. There is an algebraic number $\mu$ of degree at
most $D_{1}D_{2}$, such that the field extension $\mathbb{Q}(\mu):\mathbb{Q}$
is exactly $\mathbb{Q}(\alpha_{1},\alpha_{2}):\mathbb{Q}$.

For a collection of algebraic numbers $\alpha_{1},\ldots,\alpha_{m}$ appearing
in the input instance, by repeatedly applying this lemma, we can obtain a
simple field extension $\mathbb{Q}(\mu):\mathbb{Q}$ that can span all
$\alpha_{1},\ldots,\alpha_{m}$.

######  Lemma 2.4 ([11, Corollary 4.1.5]).

Let $\alpha$ be an algebraic number of degree $D$, and $g(z)$ an
$\mathbb{A}$-polynomial with degree $D_{g}$ and coefficients taken from
$\mathbb{Q}(\alpha):\mathbb{Q}$. There is a $\mathbb{Q}$-polynomial $f(z)$ of
degree at most $DD_{g}$, such that roots of $g(z)$ are those of $f(z)$.

The above lemma entails that roots of any $\mathbb{A}$-polynomial are also
algebraic.

######  Theorem 2.5 (Lindemann (1882) [7, Theorem 1.4]).

For any nonzero algebraic numbers $\beta_{1},\ldots,\beta_{m}$ and any
distinct algebraic numbers $\lambda_{1},\ldots,\lambda_{m}$, the sum
$\sum_{i=1}^{m}\beta_{i}\mathrm{e}^{\lambda_{i}}$ with $m\geq 1$ is nonzero.

######  Conjecture 2.6 (Schanuel (1960s) [2]).

Let $\lambda_{1},\ldots,\lambda_{m}$ be $\mathbb{Q}$-linearly independent
complex numbers. Then the field extension
$\mathbb{Q}(\lambda_{1},\mathrm{e}^{\lambda_{1}},\ldots,\lambda_{m},\mathrm{e}^{\lambda_{m}}):\mathbb{Q}$
has transcendence degree at least $m$.

Let $\mathbb{A}[z_{1},\ldots,z_{m}]$ denote the ring that contains all
$\mathbb{A}$-polynomials in variables $z_{1},\ldots,z_{m}$. Assuming
Schanuel’s conjecture, we could get:

######  Corollary 2.7 ([9, Proposition 5]).

Let $\lambda_{1},\ldots,\lambda_{m}$ be $\mathbb{Q}$-linearly independent
algebraic numbers. Then two co-prime elements $\varphi_{1}$ and $\varphi_{2}$
in the ring $\mathbb{A}[t,\exp(\lambda_{1}t),\ldots,\exp(\lambda_{m}t)]$ have
no common root except for $0$.

##  3 Quantum Continuous-Time Markov Chain

In this section, we propose the model of quantum continuous-time Markov chain
(QCTMC). We will reveal that it extends the classical continuous-time Markov
chain (CTMC). To show the practical usefulness, an example is further provided
for modelling open quantum walk.

For the sake of clarity, we start with the QCTMC without classical states:

######  Definition 3.1.

A _quantum continuous-time Markov chain_ $\mathfrak{Q}$ is a pair
$(\mathcal{H},\mathcal{L})$, in which

  * •

$\mathcal{H}$ is the Hilbert space,

  * •

$\mathcal{L}$ is the transition generator function given by a Hermitian
operator $\mathbf{H}$ and a finite set of linear operators $\mathbf{L}_{j}$ on
$\mathcal{H}$.

Usually, a density operator $\rho(0)\in\mathcal{D}$ is appointed as the
initial state of $\mathfrak{Q}$.

In the model, the transition generator function $\mathcal{L}$ gives rise to a
_universal_ way to describe the bahavior of the QCTMC, following the
generality of the Lindblad’s master equation. Thus the state $\rho(t)$ is
given by the closed-form solution to Eq. (5), i.e.,
$\mathrm{V2L}(\exp(\mathds{M}\cdot t)\cdot\mathrm{L2V}(\rho(0)))$, where
$\mathds{M}$ is the governing matrix for $\mathcal{L}$, is a computable
function from $\mathbb{R}_{\geq 0}$ to $\mathbb{C}^{d\times d}$. We notice
that $0\leq\mathrm{tr}(\mathbf{P}\rho(t))\leq 1$ holds for any projector
$\mathbf{P}$ on $\mathcal{H}$, as $\rho(t)$ is a density operator on
$\mathcal{D}$. Considering computability, the entries of $\mathbf{H}$,
$\mathbf{L}_{j}$ and $\rho(0)$ are supposed to be algebraic.

Next, we equip the QCTMC in Definition 3.1 with finitely many classical
states.

######  Definition 3.2.

A _quantum continuous-time Markov chain_ $\mathfrak{Q}$ with a finite set $S$
of classical states is a pair $(\mathcal{H}_{\mathrm{cq}},\mathcal{L})$, in
which

  * •

$\mathcal{H}_{\mathrm{cq}}:=\mathcal{C}\otimes\mathcal{H}$ is the
classical–quantum system with $\mathcal{C}=\mathrm{span}(\\{\ket{s}:s\in
S\\})$, and

  * •

$\mathcal{L}$ is the transition generator function given by a Hermitian
operator $\mathbf{H}$ and a finite set of linear operators $\mathbf{L}_{j}$ on
the enlarged $\mathcal{H}_{\mathrm{cq}}$.

Usually, a density operator
$\rho(0)\in\mathcal{D}_{\mathcal{H}_{\mathrm{cq}}}$ is appointed as the
initial state of $\mathfrak{Q}$.

In fact, the models in Definitions 3.1 and 3.2 have the same expressibility:
The QCTMC in Definition 3.1 can be obtained by setting the singleton state set
$S=\\{s\\}$ of the QCTMC in Definition 3.2; conversely, the QCTMC in
Definition 3.2 can be obtained by setting the Hilbert space as
$\mathcal{H}_{\mathrm{cq}}$ of the QCTMC in Definition 3.1. Hence, we can
freely choose one of the two definitions for convenience. As an immediate
result, using Definition 3.2, we can easily see that the QCTMC extends the
CTMC by the following lemma:

######  Lemma 3.3.

Given a CTMC $\mathfrak{C}=(S,\mathbf{Q})$, it can be modelled by a QCTMC
$\mathfrak{Q}=(\mathcal{C}\otimes\mathcal{H},\mathcal{L})$ with
$\mathcal{C}=\mathrm{span}(\\{\ket{s}:s\in S\\})$ and $\dim(\mathcal{H})=1$.

######  Proof 3.4.

It suffices to show that the states of a CTMC $\mathfrak{C}$ can be obtained
by those of some QCTMC $\mathfrak{Q}$. The state $\mathbf{x}=(x_{s})_{s\in S}$
of $\mathfrak{C}$ is given by the dynamical system
$\mathbf{x}^{\prime}(t)=\mathbf{x}(t)\cdot\mathbf{Q}$ or equivalently its
closed-form solution $\mathbf{x}(t)=\mathbf{x}(0)\cdot\exp(\mathbf{Q}\cdot
t)$, where $\mathbf{x}(0)$ is a row vector interpreted as the initial state.
We construct the QCTMC by setting Hermitian operator $\mathbf{H}=0$ and linear
operators $\mathbf{L}_{s,t}=\op{t}{s}\otimes\mathbf{Q}[s,t]$ in $Q$ for each
pair $s,t\in S$. It is not hard to validate that the state $\rho(t)$ of
$\mathfrak{Q}$ is $\mathrm{diag}(\mathbf{x}(t))$ of $\mathfrak{C}$, thus the
lemma follows.

######  Example 3.5 (Open Quantum Walk [35, 36]).

Open quantum walk (OQW) is a quantum analogy of random walk, whose system
evolution interacts with environment. For the sake of clarity, we suppose that
a particle walking along the $2$-dimensional hypercubic shown in Figure 1. The
position set is $S=\\{s_{00},s_{01},s_{10},s_{11}\\}$, where $s_{00}$ denotes
the starting position, a.k.a. the entrance, $s_{01}$ and $s_{10}$ denote
transient positions, and $s_{11}$ denotes the exit, an absorbing boundary. The
direction set is $\\{\mathrm{F},\mathrm{S}\\}$, where $\mathrm{F}$ means the
particle takes the external transition along the first coordinate, while
$\mathrm{S}$ means the particle takes the external transition along the second
coordinate. The particle will choose a direction at every moment by the inner
quantum “coin-tossing” before being absorbed. This action is implemented by
the Hadamard operator $H=\op{+}{\mathrm{F}}+\op{-}{\mathrm{S}}$ with
$\ket{\pm}=(\ket{\mathrm{F}}\pm\ket{\mathrm{S}})/\sqrt{2}$, which denotes a
fair selection between $\mathrm{F}$ and $\mathrm{S}$ as the probability
amplitudes of both directions are $\tfrac{1}{2}=(\pm 1/\sqrt{2})^{2}$.

The OQW is modelled by a QCTMC
$\mathfrak{Q}_{1}=(\mathcal{C}\otimes\mathcal{H},\mathcal{L})$ with
$\mathcal{C}=\mathrm{span}(\\{\ket{s}:s\in S\\})$, where each position in $S$
represents a classical state, and the transition function $\mathcal{L}$ is
given by the Hermitian operator $\mathbf{H}=0$ and the unique linear operator

$\displaystyle\mathbf{L}=$
$\displaystyle\op{s_{01}}{s_{00}}\otimes\op{\mathrm{S}}{-}+\op{s_{10}}{s_{00}}\otimes\op{\mathrm{F}}{+}+\op{s_{00}}{s_{01}}\otimes\op{\mathrm{S}}{-}\
+$
$\displaystyle\op{s_{11}}{s_{01}}\otimes\op{\mathrm{F}}{+}+\op{s_{00}}{s_{10}}\otimes\op{\mathrm{F}}{+}+\op{s_{11}}{s_{10}}\otimes\op{\mathrm{S}}{-}.$

For instance, when the particle is in the position $\ket{s_{00}}$, we first
apply the quantum coin-tossing $H$ to the state in $\mathcal{H}$, then we get
the result $\mathrm{F}$ or $\mathrm{S}$ leading to the position $\ket{s_{10}}$
or $\ket{s_{01}}$. The composite operations are
$(\op{\mathrm{F}}{\mathrm{F}})H=\op{\mathrm{F}}{+}$ and
$(\op{\mathrm{S}}{\mathrm{S}})H=\op{\mathrm{S}}{-}$, which makes up the first
two terms in the above $\mathbf{L}$.

From $\mathbf{L}$, we could get the governing matrix
$\mathds{M}=\mathbf{L}\otimes\mathbf{L}^{*}-\tfrac{1}{2}\mathbf{L}^{\dagger}\mathbf{L}\otimes\mathbf{I}-\tfrac{1}{2}\mathbf{I}\otimes\mathbf{L}^{\mathrm{T}}\mathbf{L}^{*}$.
Let $\rho(0)=\op{s_{00}}{s_{00}}\otimes\op{\mathrm{F}}{\mathrm{F}}$ be an
initial state. Then the states $\rho(t)$ of the OQW could be computed as
$\mathrm{V2L}(\exp(\mathds{M}\cdot t)\cdot\mathrm{L2V}(\rho(0)))$ (we omit the
detailed value due to space limit). ∎

  * $s_{01}$$s_{00}$entrance$s_{10}$$s_{11}$exitSSFFSSFF

Figure 1: A sample OQW with an absorbing boundary

  * As an absorbing boundary $s_{11}$ is introduced here, two transitions from it (in dashed line) do not exist anymore. Absorbing boundaries makes it impossible to characterise the system evolution by a closed system, i.e., using some Hermitian operator $\mathbf{H}$ only, as usual in [36]. Fortunately, we could characterise it by an open system, i.e., using the linear operators $\mathbf{L}_{j}$.

##  4 Signal Temporal Logic

Here we recall the signal temporal logic (STL) [33], which is widely used to
express real-time properties. Using it we could specify richer properties of
QCTMC than linear temporal logic (LTL) and computation tree logic (CTL) in the
time-bounded fragment.

######  Definition 4.1.

The syntax of the STL formulas are defined as follows:

$\phi:=\Phi\mid\neg\phi\mid\phi_{1}\wedge\phi_{2}\mid\phi_{1}\mathrm{U}\,^{\mathcal{I}}\phi_{2}$

in which the atomic propositions $\Phi$, interpreted as _signals_ , are of the
form $p(\mathbf{x})\in\mathbb{I}$ where $p$ is a $\mathbb{Q}$-polynomial in
$\mathbf{x}=(x_{s})_{s\in S}$ and $\mathbb{I}$ is a rational interval, and
$\mathcal{I}$ is a finite time interval. Here $\mathrm{U}\,$ is called the
until operator, and $\phi_{1}\mathrm{U}\,^{\mathcal{I}}\phi_{2}$ is the until
formula.

######  Definition 4.2.

The semantics of the STL formulas interpreted on a QCTMC $\mathfrak{Q}$ in
Definition 3.2 are given by the satisfaction relation $\models$:

$\displaystyle\rho(t)$ $\displaystyle\models\Phi$ $\displaystyle\textup{if
}p(\mathbf{x})\in\mathbb{I}\textup{ holds with
}x_{s}=\mathrm{tr}(\mathbf{P}_{s}(\rho(t))),$ $\displaystyle\rho(t)$
$\displaystyle\models\neg\phi$ $\displaystyle\textup{if
}\rho(t)\not\models\phi,$ $\displaystyle\rho(t)$
$\displaystyle\models\phi_{1}\wedge\phi_{2}$ $\displaystyle\textup{if
}\rho(t)\models\phi_{1}\wedge\rho(t)\models\phi_{2},$ $\displaystyle\rho(t)$
$\displaystyle\models\phi_{1}\mathrm{U}\,^{\mathcal{I}}\phi_{2}$
$\displaystyle\textup{if there exists a real number
}t^{\prime}\in\mathcal{I},$ $\displaystyle\textup{such that
}\forall\,t_{1}\in[t,t+t^{\prime})\,:\,\rho(t_{1})\models\phi_{1}\textup{ and
}\rho(t+t^{\prime})\models\phi_{2},$

where $\mathbf{P}_{s}$ is the projector $\op{s}{s}\otimes\mathbf{I}$ onto
classical state $s$.

From the semantics, we can see that
$\Phi_{1}\mathrm{U}\,^{\mathcal{I}_{1}}(\Phi_{2}\mathrm{U}\,^{\mathcal{I}_{2}}\Phi_{3})$
and
$(\Phi_{1}\mathrm{U}\,^{\mathcal{I}_{1}}\Phi_{2})\mathrm{U}\,^{\mathcal{I}_{2}}\Phi_{3}$
have different meanings: The former formula requires there exist
$t^{\prime}\in\mathcal{I}_{1}$ and $t^{\prime\prime}\in\mathcal{I}_{2}$ such
that $\forall\,t_{1}\in[t,t+t^{\prime}):\rho(t_{1})\models\Phi_{1}$,
$\forall\,t_{2}\in[t+t^{\prime},t+t^{\prime}+t^{\prime\prime}):\rho(t_{2})\models\Phi_{2}$
and $\rho(t+t^{\prime}+t^{\prime\prime})\models\Phi_{3}$; while the latter
formula requires there exists a $t^{\prime\prime}\in\mathcal{I}_{2}$ such that
$\rho(t+t^{\prime\prime})\models\Phi_{3}$ and for each
$t_{1}\in[t,t+t^{\prime\prime})$, there exists a
$t^{\prime}\in\mathcal{I}_{1}$ such that
$\forall\,t_{1}\in[t_{1},t_{1}+t^{\prime}):\rho(t_{1})\models\Phi_{1}$ and
$\rho(t_{1}+t^{\prime})\models\Phi_{2}$. We usually use the _parse tree_ to
clarify the structure of an STL formula $\phi$.

The logic is very generic. STL has more expressive atomic propositions than
LTL, as $\texttt{true}\equiv p(\mathbf{x})\in(-\infty,+\infty)$ and
$\texttt{false}\equiv p(\mathbf{x})\in\emptyset$. CTL has a two-stage syntax
consisting of state and path formulas. Negation and conjunction are allowed in
only state formulas, not path ones. Whereas, STL allows negation and
conjunction in any subformulas. Besides the standard Boolean calculus, we can
easily obtain a few derivations:
$\Diamond^{\mathcal{I}}\phi\equiv\texttt{true}\mathrm{U}\,^{\mathcal{I}}\phi$,
$\Box^{\mathcal{I}}\phi\equiv\neg(\Diamond^{\mathcal{I}}\neg\phi)$, and
$\phi_{1}\mathrm{R}^{\mathcal{I}}\phi_{2}\equiv\neg(\neg\phi_{1}\mathrm{U}\,^{\mathcal{I}}\neg\phi_{2})$
where $\mathrm{R}$ is the release operator.

######  Example 4.3.

Consider the open quantum walk $\mathfrak{Q}_{1}$ described in Example 3.5. It
is not hard to get the probabilities of the particle staying respectively in
$s_{00},s_{01},s_{10},s_{11}$ as follows:

$\displaystyle x_{0,0}$
$\displaystyle=\mathrm{tr}(\mathbf{P}_{s_{0,0}}(\rho(t)))=\tfrac{1}{2}\exp(-\tfrac{2+\sqrt{2}}{2}t)+\tfrac{1}{2}\exp(-\tfrac{2-\sqrt{2}}{2}t),$
$\displaystyle x_{0,1}$
$\displaystyle=\mathrm{tr}(\mathbf{P}_{s_{0,1}}(\rho(t)))=-\tfrac{\sqrt{2}}{4}\exp(-\tfrac{2+\sqrt{2}}{2}t)+\tfrac{\sqrt{2}}{4}\exp(-\tfrac{2-\sqrt{2}}{2}t)$
$\displaystyle\quad+\tfrac{1}{4}[\exp(-\tfrac{3}{2}t)-\exp(-\tfrac{1}{2}t)]\cos(\tfrac{1}{2}t)+\tfrac{1}{4}[\exp(-\tfrac{3}{2}t)+\exp(-\tfrac{1}{2}t)]\sin(\tfrac{1}{2}t),$
$\displaystyle x_{1,0}$
$\displaystyle=\mathrm{tr}(\mathbf{P}_{s_{1,0}}(\rho(t)))=-\tfrac{\sqrt{2}}{4}\exp(-\tfrac{2+\sqrt{2}}{2}t)+\tfrac{\sqrt{2}}{4}\exp(-\tfrac{2-\sqrt{2}}{2}t)$
$\displaystyle\quad-\tfrac{1}{4}[\exp(-\tfrac{3}{2}t)-\exp(-\tfrac{1}{2}t)]\cos(\tfrac{1}{2}t)-\tfrac{1}{4}[\exp(-\tfrac{3}{2}t)+\exp(-\tfrac{1}{2}t)]\sin(\tfrac{1}{2}t),$
$\displaystyle x_{1,1}$
$\displaystyle=\mathrm{tr}(\mathbf{P}_{s_{1,1}}(\rho(t)))=1+\tfrac{-1+\sqrt{2}}{2}\exp(-\tfrac{2+\sqrt{2}}{2}t)-\tfrac{1+\sqrt{2}}{2}\exp(-\tfrac{2-\sqrt{2}}{2}t).$

We can see that the probability of exiting via $s_{11}$ would be one as $t$
approaches infinity. A further question is asking how fast the particle would
reach the exit. This is actually a question about convergence performance. It
is worth monitoring the critical moment at which the probability of exiting
via $s_{11}$ equals that of staying at transient positions $s_{01},s_{10}$. A
requirement to be studied is like the following property.

> Property A: At each moment $t\in[0,5]$, whenever the probability of staying
> at $s_{01}$ or $s_{10}$ is greater than $\tfrac{1}{5}$, the probability of
> exiting via $s_{11}$ would overweight than that of staying at $s_{01}$ or
> $s_{10}$ within the coming one unit of time.

We formally specify it with the rich STL formula

$\phi_{1}\equiv\Box^{\mathcal{I}_{1}}\,(\Phi_{1}\rightarrow\Diamond^{\mathcal{I}_{2}}\Phi_{2})\equiv\neg(\texttt{true}\,\mathrm{U}\,^{\mathcal{I}_{1}}\,(\Phi_{1}\wedge\neg(\texttt{true}\,\mathrm{U}\,^{\mathcal{I}_{2}}\Phi_{2}))),$

where $\mathcal{I}_{1}=[0,5],\mathcal{I}_{2}=[0,1]$ are time intervals and
$\Phi_{1}\equiv x_{0,1}+x_{1,0}>\tfrac{1}{5},\Phi_{2}\equiv x_{1,1}\geq
x_{0,1}+x_{1,0}$ are atomic propositions, a.k.a. signals. ∎

##  5 Solving Atomic Propositions

As a basic step to decide the STL formula, we need to solve the atomic
proposition $\Phi$. That is, we will compute all solutions w.r.t. $t$, in
which $\rho(t)\models\Phi$ holds. We achieve it by a reduction to the real
root isolation for a class of real-valued functions, _exponential
polynomials_. Although real roots of exponential polynomials have been studied
in many existing literature [1, 9, 26], the ones to be isolated in this paper
involve the complicated complex exponents. So we develop a state-of-the-art
real root isolation for them, whose completeness is established on Conjecture
2.6.

Given an atomic proposition $\Phi\equiv p(\mathbf{x})\in\mathbb{I}$ (assuming
that $\mathbb{I}$ is bounded), we would like to determine the algebraic
structure of

$\varphi(t)=(p(\mathbf{x}(t))-\inf\mathbb{I})(p(\mathbf{x}(t))-\sup\mathbb{I}),$
(6)

with which we will design an algorithm for solving $\Phi\equiv
p(\mathbf{x})\in\mathbb{I}$. The structure of $\varphi(t)$ depends on that of
$x_{s}(t)=\mathrm{tr}(\mathbf{P}_{s}(\rho(t)))$. We claim that each entry of
$\rho(t)$ is of the exponential polynomial form

$\beta_{1}(t)\exp(\alpha_{1}t)+\beta_{2}(t)\exp(\alpha_{2}t)+\cdots+\beta_{m}(t)\exp(\alpha_{m}t),$
(7)

where $\beta_{1}(t),\ldots,\beta_{m}(t)$ are nonzero $\mathbb{A}$-polynomials
and $\alpha_{1},\ldots,\alpha_{m}$ are distinct algebraic numbers. It follows
the facts:

  1. 1.

The governing matrix $\mathds{M}$ in the state
$\rho(t)=\mathrm{V2L}(\exp(\mathds{M}\cdot t)\cdot\mathrm{L2V}(\rho(0)))$ of
the QCTMC takes algebraic numbers as entries.

  2. 2.

The characteristic polynomial of $\mathds{M}$ is an $\mathbb{A}$-polynomial.
The eigenvalues $\alpha_{1},\ldots,\alpha_{m}$ of $\mathds{M}$ are algebraic,
as they are roots of that $\mathbb{A}$-polynomial by Lemma 2.4. Those
eigenvalues make up all exponents in (7).

  3. 3.

The entries of the matrix exponential $\exp(\mathds{M}\cdot t)$ are in the
form (7).

The same structure holds for $x_{s}(t)$, as
$x_{s}(t)=\mathrm{tr}(\mathbf{P}_{s}(\rho(t)))$ is simply a sum of some
entries of $\rho(t)$. Furthermore, $\varphi(t)$ is also of the exponential
polynomial form (7), since it is a $\mathbb{Q}$-polynomial in
$\mathbf{x}(t)=(x_{s}(t))_{s\in S}$. If $\mathbb{I}$ is unbounded from below
(resp. above), the left (resp. right) factor could be removed from (6) for
further consideration.

Next, we will isolate all real roots $\lambda_{1},\ldots,\lambda_{n}$ of
$\varphi(t)$ in a bounded interval $\mathcal{B}$ (to be specified in the next
section). Before stating the core isolation algorithm—Algorithm 1, an overview
of the isolation procedure is provided in Fig. 2. The instances to be treated
can be roughly divided into two classes: one is trivial that can be solved by
the classical methods, e.g., [12], for ordinary polynomials; the other is
nontrivial that can be solved by Algorithm 1 but should meet three
requirements of the input in Algorithm 1. After the preprocesses Basis
Finding, Polynomialisation and Factoring, the two classes of instances can be
separated and solved by the corresponding methods.

Figure 2: Flow chart of the whole isolation procedure

The technical details along the flow chart in Fig. 2 are described below.

  * •

Basis Finding For a given set of algebraic numbers
$\\{\alpha_{1},\ldots,\alpha_{m}\\}$ extracted from the exponents of the input
exponential polynomial $\varphi(t)$, we can compute a simple extension
$\mathbb{Q}(\mu):\mathbb{Q}=\mathbb{Q}(\alpha_{1},\ldots,\alpha_{m}):\mathbb{Q}$
by Lemma 2.3, such that each $\alpha_{i}=q_{i}(\mu)$ with
$q_{i}\in\mathbb{Z}[x]$ and $\deg(q_{i})<\deg(\mu)$; and further construct a
$\mathbb{Q}$-linearly independent basis $\\{\mu_{1},\ldots,\mu_{k}\\}$ of
those exponents $\\{\alpha_{1},\ldots,\alpha_{m}\\}$ by [26, Section 3], such
that each $\alpha_{i}$ can be $\mathbb{Z}^{+}$-linearly expressed by
$\\{\mu_{1},\ldots,\mu_{k}\\}$.

  * •

Polynomialisation Thus we can get a polynomial representation
$f(t,\exp(\mu_{1}t),\ldots,\linebreak[0]\exp(\mu_{k}t))$ of $\varphi(t)$,
where $f$ is a $(k+1)$-variate polynomial with algebraic coefficients. That
is, $\varphi(t)$ is obtained by substituting
$t,\exp(\mu_{1}t),\ldots,\exp(\mu_{k}t)$ (as $k+1$ variables) into $f$.

  * •

Factoring Factoring $\varphi(t)$ into irreducible factors $\varphi_{i}(t)$
($1\leq i\leq\ell$) corresponds to factoring the $(k+1)$-variate
$\mathbb{A}$-polynomial $f$ into irreducible factors $f_{i}$ ($1\leq
i\leq\ell$), which has been implemented in polynomial time, e.g. [28].

  * •

Univariate? If the irreducible exponential polynomial $\varphi_{i}(t)$
corresponds a univariate polynomial $f_{i}$, isolating the real roots of
$\varphi_{i}(t)$ can be treated by classical methods [12]; otherwise we will
resort to Algorithm 1, for which we can infer:

    1. 1.

The exponential polynomial $\varphi(t)$ in the form (7) is plainly an
_analytic_ function that is infinitely differentiable; and it is a real-valued
function, or equivalently the imaginary part of $\varphi(t)$ is identically
zero, since each variable $x_{s}(t)$ is exactly the real-valued function
$\mathrm{tr}(\mathbf{P}_{s}\rho(t))$. The same holds for any factor
$\varphi_{i}(t)$ of $\varphi(t)$, which ensures the first requirement of the
input in Algorithm 1.

    2. 2.

By Theorem 2.5, thanks to the irreducibility of $\varphi_{i}(t)$, we have
$\varphi_{i}(\lambda)\neq 0$ holds for any
$\lambda\in\mathbb{A}\setminus\\{0\\}$, which ensures the second requirement
of the input in Algorithm 1.

    3. 3.

By Conjucture 2.6 and Corollary 2.7, each irreducible factor $\varphi_{i}(t)$
and its derivative $\varphi_{i}^{\prime}(t)$ are co-prime, and thus have no
common real root except for $0$, which ensures the last requirement of the
input in Algorithm 1.

  * •

Refinement After performing Algorithm 1 with each individual irreducible
factor $\varphi_{i}(t)$ of $\varphi(t)$, we would obtain a list of disjoint
isolation intervals $\mathcal{I}_{i,1},\ldots,\mathcal{I}_{i,n_{i}}$. The
isolation intervals of different irreducible factors may be overlapping.
However, by Corollary 2.7 again, we have that each pair of co-prime factors of
$\varphi(t)$ has no common real root except for $0$. So all these isolation
intervals $\mathcal{I}_{i,1},\ldots,\mathcal{I}_{i,n_{i}}$ ($1\leq i\leq\ell$)
can be further refined to be pairwise disjoint. That would be the complete
list of isolation intervals $\mathcal{I}_{1},\ldots,\mathcal{I}_{n}$ for
$\varphi(t)$, and thereby completes the whole isolation procedure.

Algorithm 1 Real Root Isolation for a Real-valued Function

1: $\\{\mathcal{I}_{1},\ldots,\mathcal{I}_{n}\\}\Leftarrow{\sf
Isolate}(\varphi,\mathcal{I})$

2:$\varphi(t)$ is a real-valued function defined on a rational interval
$\mathcal{I}=[l,u]$, satisfying:

  1. 1.

$\varphi(t)$ is twice-differentiable,

  2. 2.

$\varphi(t)$ has no rational root in $\mathcal{I}$, and

  3. 3.

$\varphi(t)$ and $\varphi^{\prime}(t)$ have no common real root in
$\mathcal{I}$.

3:$\mathcal{I}_{1},\ldots,\mathcal{I}_{n}$ are finitely many disjoint
intervals, such that each contains exactly one real root of $\varphi$ in
$\mathcal{I}$, and together contain all.

4:compute an upper bound $M$ of
$\\{|\varphi^{\prime}(t)|\,:\,t\in\mathcal{I}\\}$;

5:compute an upper bound $M^{\prime}$ of
$\\{|\varphi^{\prime\prime}(t)|\,:\,t\in\mathcal{I}\\}$;

6:$i\leftarrow 0$, $N\leftarrow 2$ and $\delta\leftarrow(u-l)/N$;
$\triangleright$ Here $N>1$ is a free parameter to indicate the number of
subintervals to be split. We predefine it simply as $2$.

7:while $i\leq N$ do

8: if $|\varphi(l+i\delta)|>M\delta$ then $i\leftarrow i+1$; $\triangleright$
$\varphi$ has no local real root

9: else if $|\varphi(l+i\delta+\delta)|>M\delta$ then $i\leftarrow i+2$;
$\triangleright$ $\varphi$ has no local real root

10: else if $|\varphi^{\prime}(l+i\delta)|\geq M^{\prime}\delta$ then
$\triangleright$ $\varphi$ is locally monotonic

11: if $\varphi(l+i\delta)\varphi(l+i\delta+\delta)<0$ then output
$(l+i\delta,l+i\delta+\delta)$;

12: $i\leftarrow i+1$;

13: else if $|\varphi^{\prime}(l+i\delta+\delta)|\geq M^{\prime}\delta$ then
$\triangleright$ $\varphi$ is locally monotonic

14: if $\varphi(l+i\delta)\varphi(l+i\delta+2\delta)<0$ then output
$(l+i\delta,l+i\delta+2\delta)$;

15: $i\leftarrow i+2$;

16: else

17: ${\sf Isolate}(\varphi,[l+i\delta,l+i\delta+\delta])$;

18: $i\leftarrow i+1$.

#### Soundness of Algorithm 1

We justify three groups of treatment in the loop body in turn.

  1. 1.

If the condition in Line 8 (resp. 9) holds, $\varphi$ has no real root in the
neighborhood centered at $l+i\delta$ (resp. $l+(i+1)\delta$) with radius
$\delta$. So we exclude the neighborhood.

  2. 2.

If the condition in Line 10 (resp. 13) holds, $\varphi$ is monotonic in the
neighborhood centered at $l+i\delta$ (resp. $l+(i+1)\delta$) with radius
$\delta$. Then, if the condition in Line 11 (resp. 14) holds, i.e. $\varphi$
has different signs at endpoints of the neighborhood, the unique real root in
the neighborhood exists and should be output; otherwise we just exclude the
neighborhood.

  3. 3.

If it is not in the two decisive cases listed above, we perform Algorithm 1
recursively in a subinterval $[l+i\delta,l+(i+1)\delta]$ of $[l,u]$. ∎

#### Completeness of Algorithm 1

The termination of Algorithm 1 entails the completeness. In other words, it
suffices to show that for any real-valued function $\varphi$ that satisfies
the requirements, Algorithm 1 can always output all real roots of $\varphi$
within a finitely many times of recursion. Since $\varphi$ and
$\varphi^{\prime}$ are real-valued functions defined on the closed and bounded
interval $\mathcal{I}$ and they have no common real root in $\mathcal{I}$,
there is a positive constant $\tau$, such that either $|\varphi|\geq\tau$ or
$|\varphi^{\prime}|\geq\tau$ holds everywhere of $\mathcal{I}$. Then, at any
point $c$ in $\mathcal{I}$, we can get a neighborhood with constant radius
$rad:=\min(\tau/M,\tau/M^{\prime})$, in which either $\varphi$ has no real
root or is monotonic. So the two decisive cases must take place, provided that
the subinterval has length not greater than $rad$. It implies that the
recursion depth of Algorithm 1 is bounded by
$\lceil\log_{2}(\|\mathcal{I}\|/rad)\rceil$, where
$\|\mathcal{I}\|=\sup\mathcal{I}-\inf\mathcal{I}$. Hence the termination is
guaranteed. ∎

After obtaining all real roots $\lambda_{1},\ldots,\lambda_{n}$ of
$\varphi(t)$ in the bounded interval $\mathcal{B}$ by Algorithm 1, we have
that on each interval $\mathcal{J}_{i}$ ($0\leq i\leq n$) of the $n+1$
intervals in $\mathcal{B}\setminus\\{\lambda_{1},\ldots,\lambda_{n}\\}$:

$[\inf\mathcal{B},\lambda_{1}),(\lambda_{1},\lambda_{2}),\ldots,(\lambda_{n-1},\lambda_{n}),(\lambda_{n},\sup\mathcal{B}],$
(8)

$p(\mathbf{x}(t))\in\mathbb{I}$ holds everywhere of $t\in\mathcal{J}_{i}$ or
nowhere. Finally, we can obtain the desired solution set $\mathbb{J}$ (to be
used in the next section) of $p(\mathbf{x}(t))\in\mathbb{I}$ by a finite union
as follows

$\bigcup_{\begin{subarray}{c}0\leq i\leq n\\\
p(\mathbf{x}(\mathcal{J}_{i}))\subseteq\mathbb{I}\end{subarray}}\mathcal{J}_{i}\cup\bigcup_{\begin{subarray}{c}1\leq
i\leq n\\\
p(\mathbf{x}(\lambda_{i}))\in\mathbb{I}\end{subarray}}\\{\lambda_{i}\\}.$ (9)

######  Example 5.1.

Reconsider Example 4.3. The exponential polynomial extracted from $\Phi_{1}$
is

$\varphi_{1}(t)=x_{0,1}(t)+x_{1,0}(t)-\tfrac{1}{5}=-\tfrac{1}{5}-\tfrac{\sqrt{2}}{2}\exp(-\tfrac{2+\sqrt{2}}{2}t)+\tfrac{\sqrt{2}}{2}\exp(-\tfrac{2-\sqrt{2}}{2}t),$

and the exponential polynomial extracted from $\Phi_{2}$ is

$\varphi_{2}(t)=x_{1,1}(t)-x_{0,1}(t)-x_{1,0}(t)=1+(\sqrt{2}-\tfrac{1}{2})\exp(-\tfrac{2+\sqrt{2}}{2}t)-(\sqrt{2}+\tfrac{1}{2})\exp(-\tfrac{2-\sqrt{2}}{2}t).$

To solve $\Phi_{1}$ and $\Phi_{2}$ in a bounded interval, say
$\mathcal{B}=[0,6]$, we need to determine the real roots of $\varphi_{1}$ and
$\varphi_{2}$. Since both $\varphi_{1}$ and $\varphi_{2}$ are irreducible and
their corresponding polynomial representations are bivariate, they have no
rational root, repeated real root, nor common real root. After invoking
Algorithm 1 on $\varphi_{1}$ with $\mathcal{B}$, we obtain two isolation
intervals $[0,\tfrac{25}{64}]$ (containing real root $\lambda_{1}\approx
0.352097$) and $[\tfrac{275}{64},\tfrac{575}{128}]$ (containing
$\lambda_{2}\approx 4.49181$), which could be easily refined up to any
precision. For $\varphi_{2}$, as $\varphi_{2}(0)=0$, we make a slight shift on
the left endpoint of $\mathcal{B}$ in the consideration, e.g.,
$[\tfrac{1}{1000},6]$. After invoking Algorithm 1 on $\varphi_{2}$ with
$[\tfrac{1}{1000},6]$, we could get the unique isolation intervals
$[\tfrac{125059}{64000},\tfrac{275117}{128000}]$, which contains the real root
$\lambda_{3}\approx 2.14897$. The three isolation intervals are pairwise
disjoint.

Finally, we have that the solution set of $\Phi_{1}$ is
$(\lambda_{1},\lambda_{2})$ in $\mathcal{B}$, and the solution set of
$\Phi_{2}$ is $\\{0\\}\cup[\lambda_{3},6]$. ∎

Under Conjecture 2.6, we get the following computability result while the
complexity is still an open problem as left in existing literature [9, 26].

######  Lemma 5.2.

The atomic propositions in STL are solvable over QCTMCs.

In fact, Conjecture 2.6 is a powerful tool to treat roots of the general
exponential polynomial. For some special subclasses of exponential
polynomials, there are solid theorems to treat them: one is Theorem 2.5 that
has been employed [1] for the exponential polynomials in the ring
$\mathbb{Q}[t,\exp(t)]$, the other is the Gelfond–Schneider theorem employed
[26, Subsection 4.1] for the exponential polynomials in
$\mathbb{Q}[\exp(\mu_{1}t),\exp(\mu_{2}t)]$ where $\mu_{1}$ and $\mu_{2}$ are
_two_ $\mathbb{Q}$-linear independent _real_ algebraic numbers. In Example
5.1, the Gelfond–Schneider theorem is sufficient to treat roots of the
exponential polynomials $\varphi_{1}$ and $\varphi_{2}$, thus the termination
is guaranteed. Algorithm 1 can isolate roots of elements in
$\mathbb{Q}[t,\exp(\mu_{1}t),\ldots,\exp(\mu_{k}t)]$ for _arbitrarily many_
$\mathbb{Q}$-linear independent _complex_ algebraic numbers
$\mu_{1},\ldots,\mu_{k}$. Additionally, Conjecture 2.6 has been employed to
isolate simple roots of more expressible functions than exponential
polynomials [38, 39], but fails to find repeated roots. Hence, this paper
makes a trade-off between the expressibility of functions and the completeness
of methodologies.

##  6 Checking STL Formulas

In the previous section, we have solved atomic propositions. Now we consider
the general STL formula $\phi$. For a given formula $\phi$, we compute the so-
called _post-monitoring period_ $\mathrm{mnt}(\phi)$, independent on the
initial time $t_{0}$, such that the truth of $\rho(t_{0})\models\phi$ could be
affected by those $\rho(t)$ with $t\in[t_{0},t_{0}+\mathrm{mnt}(\phi)]$. Then
we decide $\phi$ with a bottom-up fashion. The complexity turns out to be
linear in the size $\|\phi\|$ of the input STL formula $\phi$, which is
defined as the number of logic connectives in $\phi$ as standard.

Given an STL formula $\phi$, we need to post-monitor a time period to decide
the truth of $\rho(t_{0})\models\phi$ at an initial time $t_{0}$, especially
for the until formula $\phi_{1}\mathrm{U}\,^{\mathcal{I}}\phi_{2}$. For
example, according to the semantics of STL, to decide
$\rho(t_{0})\models\phi_{2}$ with
$\phi_{2}\equiv\Phi_{1}\mathrm{U}\,^{\mathcal{I}_{1}}(\Phi_{2}\mathrm{U}\,^{\mathcal{I}_{2}}\Phi_{3})$,
we have to monitor the states $\rho(t)$ from time $t_{0}$ to
$t_{0}+\sup\mathcal{I}_{1}+\sup\mathcal{I}_{2}$. It inspires us to calculate
the post-monitoring period $\mathrm{mnt}(\phi)$ as

$\mathrm{mnt}(\phi)=\begin{cases}0&\textup{if }\phi=\Phi,\\\
\mathrm{mnt}(\phi_{1})&\textup{if }\phi=\neg\phi_{1},\\\
\max(\mathrm{mnt}(\phi_{1}),\mathrm{mnt}(\phi_{2}))&\textup{if
}\phi=\phi_{1}\wedge\phi_{2},\\\
\sup\mathcal{I}+\max(\mathrm{mnt}(\phi_{1}),\mathrm{mnt}(\phi_{2}))&\textup{if
}\phi=\phi_{1}\mathrm{U}\,^{\mathcal{I}}\phi_{2}.\end{cases}$ (10)

######  Lemma 6.1.

Given an STL formula $\phi$, the satisfaction $\rho(t_{0})\models\phi$ is
entirely determined by the states $\rho(t)$ with $t_{0}\leq t\leq
t_{0}+\mathrm{mnt}(\phi)$.

######  Proof 6.2.

We discuss it upon the syntactical structure of the STL formula $\phi$.

For the atomic proposition $\Phi$, $\rho(t_{0})\models\Phi$ is plainly
determined by $\rho(t_{0})$.

For the negation $\neg\phi_{1}$, if $\rho(t_{0})\models\phi_{1}$ is determined
by $\rho(t)$ with $t_{0}\leq t\leq t_{0}+\mathrm{mnt}(\phi_{1})$, so is
$\rho(t_{0})\models\neg\phi_{1}$.

For the conjunction $\phi_{1}\wedge\phi_{2}$, if $\rho(t_{0})\models\phi_{1}$
(resp. $\rho(t_{0})\models\phi_{2}$) is determined by $\rho(t)$ with
$t_{0}\leq t\leq t_{0}+\mathrm{mnt}(\phi_{1})$ (resp. $t_{0}\leq t\leq
t_{0}+\mathrm{mnt}(\phi_{2})$), $\rho(t_{0})\models\phi_{1}\wedge\phi_{2}$ is
determined by the union of those states, i.e. $\rho(t)$ with $t_{0}\leq t\leq
t_{0}+\max(\mathrm{mnt}(\phi_{1}),\mathrm{mnt}(\phi_{2}))$.

For the until formula $\phi_{1}\mathrm{U}\,^{\mathcal{I}}\phi_{2}$, if
$\rho(t_{0})\models\phi_{1}$ (resp. $\rho(t_{0})\models\phi_{2}$) is
determined by $\rho(t)$ with $t_{0}\leq t\leq t_{0}+\mathrm{mnt}(\phi_{1})$
(resp. $t_{0}\leq t\leq t_{0}+\mathrm{mnt}(\phi_{2})$),
$\rho(t_{0})\models\phi_{1}\mathrm{U}\,^{\mathcal{I}}\phi_{2}$ is determined
by $\rho(t)$ with $t_{0}\leq t\leq
t_{0}+\sup\mathcal{I}+\max(\mathrm{mnt}(\phi_{1}),\mathrm{mnt}(\phi_{2}))$,
where $\sup\mathcal{I}$ is caused by the admissible transition at the latest
time in the until formula, since then we have to determine
$\rho(t)\models\phi_{1}$ from time $t_{0}$ to $t_{0}+\sup\mathcal{I}$ and
determine $\rho(t_{0}+\sup\mathcal{I})\models\phi_{2}$.

To decide $\rho(0)\models\phi$, our method is based on the parse tree
$\mathcal{T}$ of $\phi$ as follows.

Basically, for each leaf of $\mathcal{T}$ that represents an atomic
proposition $\Phi$, we compute the solution set $\mathbb{J}$ (possibly a union
of maximal solution intervals $\mathcal{J}$) of $\Phi$ within the monitoring
interval $\mathcal{B}:=[0,\mathrm{mnt}(\phi)]$ by Algorithm 1.

Inductively, for each intermediate node of $\mathcal{T}$ that represents the
subformula $\psi$ of $\phi$, we tackle it into three classes.

  * •

If $\psi=\neg\phi_{1}$, supposing that $\mathbb{J}_{1}$ is the solution set of
$\phi_{1}$, the solution set $\mathbb{J}^{\prime}$ of $\psi$ is
$\mathcal{B}\setminus\mathbb{J}_{1}$.

  * •

If $\psi=\phi_{1}\wedge\phi_{2}$, supposing that $\mathbb{J}_{1}$ (resp.
$\mathbb{J}_{2}$) is the solution set of $\phi_{1}$ (resp. $\phi_{2}$), the
solution set $\mathbb{J}^{\prime}$ of $\psi$ is
$\mathbb{J}_{1}\cap\mathbb{J}_{2}$.

  * •

If $\psi=\phi_{1}\mathrm{U}\,^{\mathcal{I}}\phi_{2}$, supposing that
$\mathbb{J}_{1}$ (resp. $\mathbb{J}_{2}$) is the solution set of $\phi_{1}$
(resp. $\phi_{2}$), the solution set $\mathbb{J}^{\prime}$ of $\psi$ is

$\\{t:(t^{\prime}\in\mathcal{I})\wedge([t,t+t^{\prime})\subseteq\mathbb{J}_{1})\wedge(t+t^{\prime}\in\mathbb{J}_{2})\\}.$

directly from the semantics of the until formula
$\phi_{1}\mathrm{U}\,^{\mathcal{I}}\phi_{2}$ in Definition 4.2, as

    * –

$[t,t+t^{\prime})\subseteq\mathbb{J}_{1}$ if and only if
$\forall\,t_{1}\in[t,t+t^{\prime})\,:\,\rho(t_{1})\models\phi_{1}$, and

    * –

$t+t^{\prime}\in\mathbb{J}_{2}$ if and only if
$\rho(t+t^{\prime})\models\phi_{2}$.

Note that the inductive steps of the above procedure do not generally produce
all solutions of the subformula $\psi$ in $\mathcal{B}$. Since by Lemma 6.1
$\rho(t_{0})\models\psi$ is entirely determined by $\rho(t)$ with $t_{0}\leq
t\leq t_{0}+\mathrm{mnt}(\psi)$, the resulting solution set
$\mathbb{J}^{\prime}$ contains all solutions of $\psi$ in
$[0,\mathrm{mnt}(\phi)-\mathrm{mnt}(\psi)]$ and possibly misses some solutions
in the right subinterval
$(\mathrm{mnt}(\phi)-\mathrm{mnt}(\psi),\mathrm{mnt}(\phi)]$. Anyway, the
subinterval $[0,\mathrm{mnt}(\phi)-\mathrm{mnt}(\psi)]$ has the left-closed
endpoint $0$, which suffices to decide $\rho(0)\models\phi$.

With a bottom-up fashion, we could eventually get the solution set
$\mathbb{J}$ of $\phi$, by which $\rho(0)\models\phi$ can be decided to be
true if and only if $0\in\mathbb{J}$. Overall, the procedure costs $\|\phi\|$
times of the interval operations and at most $\|\phi\|$ times of calling
Algorithm 1 for getting the solution set of an atomic proposition. That is,
the query complexity of model checking STL formulas is linear in $\|\phi\|$ by
calling Algorithm 1. The query complexity addresses the issue of the number of
calls to a black box routine with unknown complexities and is commonly used in
quantum computing, where the routine is usually called an oracle. For example,
oracles can be a procedure of encoding an entry of a matrix into a quantum
state [25] or a quantum circuit of preparing a specific quantum state [22].

######  Example 6.3.

For the STL formula
$\phi_{1}\equiv\neg(\texttt{true}\,\mathrm{U}\,^{\mathcal{I}_{1}}\,(\Phi_{1}\wedge\neg(\texttt{true}\,\mathrm{U}\,^{\mathcal{I}_{2}}\Phi_{2})))$,
the post-monitoring period $\mathrm{mnt}(\phi_{1})$ is
$\sup\mathcal{I}_{1}+\sup\mathcal{I}_{2}=6$ by Eq. (10), implying
$\mathcal{B}=[0,6]$ as used in Example 5.1. We construct the parse tree of
$\phi_{1}$ in Figure 3. Based on it, we could calculate the solution sets of
all nodes in a bottom-up fashion:

  * •

Basically, the solution set for $\Phi_{1}$ is $(\lambda_{1},\lambda_{2})$
where $\lambda_{1}\approx 0.352097$ and $\lambda_{2}\approx 4.49181$, the
solution set for $\Phi_{2}$ is $\\{0\\}\cup[\lambda_{3},6]$ where
$\lambda_{3}\approx 2.14897$, and the solution set for true is plainly
$[0,6]$. The post-monitoring periods of the three leaves are $0$. Since
$\mathcal{B}$ is $[0,6]$, we have got all the solutions in $[0,6]$.

  * •

The solution set for $\texttt{true}\,\mathrm{U}\,^{\mathcal{I}_{2}}\Phi_{2}$
is $[\lambda_{3}-1,6]$, and that for the negation is $[0,\lambda_{3}-1)$. The
post-monitoring periods of the two nodes are $1$, thus we have got all
solutions in $[0,5]$.

  * •

The solution set for
$\Phi_{1}\wedge\neg(\texttt{true}\,\mathrm{U}\,^{\mathcal{I}_{2}}\Phi_{2})$ is
$(\lambda_{1},\lambda_{3}-1)$. Its post-monitoring period is $1$, thus we have
got all solutions in $[0,5]$.

  * •

Finally, the solution set for
$\texttt{true}\,\mathrm{U}\,^{\mathcal{I}_{1}}\,(\Phi_{1}\wedge\neg(\texttt{true}\,\mathrm{U}\,^{\mathcal{I}_{2}}\Phi_{2}))$
is $[0,\lambda_{3}-1)$, and that for the negation (the root, representing the
whole STL formula $\phi_{1}$) is $[\lambda_{3}-1,6]$. Their post-monitoring
periods are $6$, thus we have got the solution in $[0,0]$.

Since $0\notin[\lambda_{3}-1,6]$, we can decide $\rho(0)\models\phi_{1}$ to be
false. Hence the particle walking along Figure 1 does not satisfy the desired
convergence performance—Property A. ∎

$\neg$$\mathrm{U}\,^{\mathcal{I}_{1}}$$\wedge$true$\neg$$\Phi_{1}$$\mathrm{U}\,^{\mathcal{I}_{2}}$$\Phi_{2}$true
Figure 3: Parse tree of the STL formula $\phi_{1}$

Finally, under Conjecture 2.6, we obtain the main result:

######  Theorem 6.4.

The STL formulas are decidable over QCTMCs.

##  7 Concluding Remarks

In this paper, we introduced the model of QCTMC that extends CTMC, and
established the decidability of the STL formulas over it. To this goal, we
firstly solved the atomic propositions in STL by real root isolation of a wide
class of exponential polynomials, whose completeness was based on Schanuel’s
conjecture. Then we decided the general STL formula using 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 developed state-of-art real root
isolation routine. We demonstrated our method by a running example of an open
quantum walk.

For future work, we would like to explore the following aspects:

  * •

how to apply the proposed method to verify non-Markov models in the real world
[35];

  * •

how to design an efficient numerical approximation of the exact method in this
paper;

  * •

and checking other formal logics, e.g. [3], over the QCTMC.

## References

  * [1] M. Achatz, S. McCallum, and V. Weispfenning.  Deciding polynomial–exponential problems.  In Proc. 33rd International Symposium on Symbolic and Algebraic Computation, ISSAC 2008, pages 215–222. ACM Press, 2008.
  * [2] J. Ax.  On Schanuel’s conjectures.  Annals of Mathematics, 93(2):252–268, 1971.
  * [3] A. Aziz, K. Sanwal, V. Singhal, and R. Brayton.  Verifying continuous time Markov chains.  In Computer Aided Verification: 8th International Conference, CAV’96, volume 1102 of LNCS, pages 269–276. Springer, 1996.
  * [4] A. Aziz, K. Sanwal, V. Singhal, and R. Brayton.  Model-checking continous-time Markov chains.  ACM Transactions on Computational Logic, 1(1):162–170, 2000.
  * [5] C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen.  Model-checking algorithms for continuous-time Markov chains.  IEEE Transactions on Software Engineering, 29(6):524–541, 2003\.
  * [6] C. Baier, J.-P. Katoen, and H. Hermanns.  Approximate symbolic model checking of continuous-time Markov chains.  In CONCUR’99 Concurrency Theory, volume 1664 of LNCS, pages 146–161. Springer, 1999.
  * [7] A. Baker.  Transcendental Number Theory.  Cambridge University Press, 1975.
  * [8] B. Baumgartner and H. Narnhofer.  The structures of state space concerning quantum dynamical semigroups.  Reviews in Mathematical Physics, 24(02):article no. 1250001, 2012\.
  * [9] V. Chonev, J. Ouaknine, and J. Worrell.  On the Skolem problem for continuous linear dynamical systems.  In 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, volume 55 of LIPIcs, pages 100:1–100:13. Schloss Dagstuhl, 2016.
  * [10] G. I. Cirillo and F. Ticozzi.  Decompositions of Hilbert spaces, stability analysis and convergence probabilities for discrete-time quantum dynamical semigroups.  Journal of Physics A: Mathematical and Theoretical, 48(8):article no. 085302, 2015.
  * [11] H. Cohen.  A Course in Computational Algebraic Number Theory.  Springer, 1996.
  * [12] G. E. Collins and R. Loos.  Polynomial real root isolation by differentiation.  In Proc. SYMSAC 1976, pages 15–25. ACM Press, 1976.
  * [13] C. Dehnert, S. Junges, J.-P. Katoen, and M. Volk.  A Storm is coming: A modern probabilistic model checker.  In Computer Aided Verification - 29th International Conference, CAV 2017, Part II, volume 10427 of LNCS, pages 592–600. Springer, 2017\.
  * [14] Y. Feng, E. M. Hahn, A. Turrini, and S. Ying.  Model checking $\omega$-regular properties for quantum Markov chains.  In 28th International Conference on Concurrency Theory, CONCUR 2017, volume 85 of LIPIcs, pages 35:1–35:16. Schloss Dagstuhl, 2017.
  * [15] Y. Feng, N. Yu, and M. Ying.  Model checking quantum Markov chains.  Journal of Computer and System Sciences, 79(7):1181–1198, 2013\.
  * [16] S. J. Gay, R. Nagarajan, and N. Papanikolaou.  Probabilistic model-checking of quantum protocols.  In Proc. 2nd International Workshop on Developments in Computational Models, 2006.  available at http://arxiv.org/abs/quant-ph/0504007.
  * [17] S. J. Gay, R. Nagarajan, and N. Papanikolaou.  QMC: A model checker for quantum systems.  In Computer Aided Verification, 20th International Conference, CAV 2008, volume 5123 of LNCS, pages 543–547. Springer, 2008.
  * [18] S. Goldstein, J. L. Lebowitz, R. Tumulka, and N. Zanghì.  Long-time behavior of macroscopic quantum systems.  The European Physical Journal H, 35(2):173–200, 2010.
  * [19] V. Gorini, A. Kossakowski, and E. C. G. Sudarshan.  Completely positive dynamical semigroups of $n$-level systems.  Journal of Mathematical Physics, 17(5):821–825, 1976.
  * [20] J. Guan, Y. Feng, A. Turrini, and M. Ying.  Model checking applied to quantum physics.  CoRR, abs/1902.03218, 2019.  URL: https://arxiv.org/abs/1902.03218.
  * [21] J. Guan, Y. Feng, and M. Ying.  Decomposition of quantum Markov chains and its applications.  Journal of Computer and System Sciences, 95:55–68, 2018.
  * [22] J. Guan, Q. Wang, and M. Ying.  An HHL-based algorithm for computing hitting probabilities of quantum walks.  Quantum Information and Computation, 2021(5&6):0395–0408, 2021\.
  * [23] J. Guan and N. Yu.  Verification of continuous-time Markov chains.  CoRR, abs/2004.08059, 2020.  URL: https://arxiv.org/abs/2004.08059.
  * [24] E. M. Hahn, Y. Li, S. Schewe, A. Turrini, and L. Zhang.  iscasMc: A web-based probabilistic model checker.  In FM 2014: Formal Methods—19th International Symposium, volume 8442 of LNCS, pages 312–317. Springer, 2014.
  * [25] A. W. Harrow, A. Hassidim, and S. Lloyd.  Quantum algorithm for linear systems of equations.  Physical Review Letters, 103(15):article no. 150502, 2009.
  * [26] C.-C. Huang, J.-C. Li, M. Xu, and Z.-B. Li.  Positive root isolation for poly-powers by exclusion and differentiation.  Journal of Symbol Computation, 85:148–169, 2018.
  * [27] T. Kailath.  Linear Systems.  Prentice Hall, 1980.
  * [28] E. Kaltofen.  Polynomial-time reductions from multivariate to bi- and univariate integral polynomial factorization.  SIAM Journal on Computing, 14(2):469–489, 1985.
  * [29] M. Kwiatkowska, G. Norman, and D. Parker.  PRISM 4.0: Verification of probabilistic real-time systems.  In Computer Aided Verification: 23rd International Conference, CAV 2011, volume 6806 of LNCS, pages 585–591. Springer, 2011.
  * [30] L. Li and Y. Feng.  Quantum Markov chains: Description of hybrid systems, decidability of equivalence, and model checking linear-time properties.  Information and Computation, 244:229–244, 2015.
  * [31] G. Lindblad.  On the generators of quantum dynamical semigroups.  Communications in Mathematical Physics, 48(2):119–130, 1976.
  * [32] R. Loos.  Computing in algebraic extensions.  In Computer Algebra: Symbolic and Algebraic Computation, pages 173–187. Springer, 1983.
  * [33] O. Maler and D. Nickovic.  Monitoring temporal properties of continuous signals.  In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, volume 3253 of LNCS, pages 152–166. Springer, 2004\.
  * [34] M. A. Nielsen and I. L. Chuang.  Quantum Computation and Quantum Information.  Cambridge University Press, 2000.
  * [35] C. Pellegrini.  Continuous time open quantum random walks and non-Markovian Lindblad master equations.  Journal of Statistical Physics, 154:838–865, 2014.
  * [36] I. Sinayskiy and F. Petruccione.  Microscopic derivation of open quantum walks.  Physical Review A, 92(3):article no. 032105, 2015.
  * [37] W. J. Stewart.  Introduction to the Numerical Solution of Markov Chains.  Princeton University Press, 1994.
  * [38] A. Strzeboński.  Real root isolation for exp–log functions.  In Proc. 33rd. International Symposium on Symbolic and Algebraic Computation, ISSAC 2008, pages 303–313. ACM Press, 2008.
  * [39] A. Strzeboński.  Real root isolation for tame elementary functions.  In Proc. 34th International Symposium on Symbolic and Algebraic Computation, ISSAC 2009, pages 341–350. ACM Press, 2009.
  * [40] M. M. Wolf.  Quantum channels & operations: Guided tour.  Lecture notes available at http://www-m5.ma.tum.de/foswiki/pubM, 5, 2012.
  * [41] M. Xu, C.-C. Huang, and Y. Feng.  Measuring the constrained reachability in quantum Markov chains.  Acta Informatica, online first, 2021.
  * [42] M. Xu, L. Zhang, D. N. Jansen, H. Zhu, and Z. Yang.  Multiphase until formulas over Markov reward models: An algebraic approach.  Theoretical Computer Science, 611:116–135, 2016.
  * [43] M. Ying and Y. Feng.  Model-checking quantum systems.  National Science Review, 6(1):28–31, 2019.
  * [44] M. Ying and Y. Feng.  Model Checking Quantum Systems: Principles and Algorithms.  Cambridge University Press, 2021.
  * [45] S. Ying, Y. Feng, N. Yu, and M. Ying.  Reachability probabilities of quantum Markov chains.  In CONCUR 2013: Concurrency Theory—24th International Conference, volume 8052 of LNCS, pages 334–348. Springer, 2013.
  * [46] L. Zhang, D. N. Jansen, F. Nielson, and H. Hermanns.  Automata-based CSL model checking.  In Automata, Languages and Programming: 38th International Colloquium, ICALP 2011, Part II, volume 6756 of LNCS, pages 271–282. Springer, 2011.
  * [47] L. Zhang, D. N. Jansen, F. Nielson, and H. Hermanns.  Efficient CSL model checking using stratification.  Logical Methods in Computer Science, 8(2:17):1–18, 2012.