11institutetext:  Key Laboratory of System Software (Chinese Academy of
Sciences) and State Key Laboratory of Computer Science, Institute of Software,
Chinese Academy of Sciences, Beijing 100190, China
<EMAIL_ADDRESS>22institutetext: Department of Computer Science and
Technology, Tsinghua University, Beijing 100084, China 33institutetext:
Institute of Intelligent Software, Guangzhou, Guangzhou 511458, China
44institutetext: The Centre for Quantum Software and Information, University
of Technology Sydney, NSW 2007, Australia.

# Measurement-based Verification of Quantum Markov Chains

Ji Guan(B) 11 Yuan Feng 22 Andrea Turrini(B) 1133 Mingsheng Ying 44

###### Abstract

Model-checking techniques have been extended to analyze quantum programs and
communication protocols represented as quantum Markov chains, an extension of
classical Markov chains. To specify qualitative temporal properties, a
subspace-based quantum temporal logic is used, which is built on Birkhoff–von
Neumann atomic propositions. These propositions determine whether a quantum
state is within a subspace of the entire state space. In this paper, we
propose the measurement-based linear-time temporal logic MLTL to check
quantitative properties. MLTL builds upon classical linear-time temporal logic
(LTL) but introduces quantum atomic propositions that reason about the
probability distribution after measuring a quantum state. To facilitate
verification, we extend the symbolic dynamics-based techniques for stochastic
matrices described by Agrawal et al. (JACM 2015) to handle more general
quantum linear operators (super-operators) through eigenvalue analysis. This
extension enables the development of an efficient algorithm for approximately
model checking a quantum Markov chain against an MLTL formula. To demonstrate
the utility of our model-checking algorithm, we use it to simultaneously
verify linear-time properties of both quantum and classical random walks.
Through this verification, we confirm the previously established advantages
discovered by Ambainis et al. (STOC 2001) of quantum walks over classical
random walks and discover new phenomena unique to quantum walks.

##  1 Introduction

Model checking is a formal verification technique that is used to ensure the
correctness of a system based on a given specification [1]. In recent years,
model checking has been applied to quantum systems and has become a powerful
tool for verifying the behaviors and properties of quantum programs or
communication protocols [2, 3]. Similar to the classical case, the main
components of model checking quantum systems are the system model and the
temporal logic, which are used to mathematically describe the evolution of the
system and specify its temporal properties, respectively.

System Model. Quantum Markov Chains (QMCs), which are the quantum extension of
classical _Markov chains_ (MCs), provide an exceptional paradigm for modeling
the evolution of quantum systems in various scenarios, including quantum
control [4], quantum information theory [5], quantum programming [6], and
quantum communication systems [7]. Notably, quantum walks, which are a special
class of QMCs, have been successfully employed in the design of quantum
algorithms (for a survey of this research line, see [8, 9]). A QMC
$\mathcal{Q}$ is defined as a triple
$\mathcal{Q}=(\mathcal{H},\mathcal{E},\rho_{0})$ that corresponds to a
classical Markov chain $(S,P,s_{0})$, where $\mathcal{H}$ is a finite-
dimensional Hilbert (linear) state space instead of the finite state set $S$,
$\mathcal{E}$ is a _super-operator_ on $\mathcal{H}$ instead of the transition
stochastic matrix $P$ on $S$, and $\rho_{0}$, which is a _density matrix_ ,
represents the initial state instead of $s_{0}$. Intuitively, the super-
operator $\mathcal{E}(\,\mathord{\cdot}\,)$, which is a linear mapping, models
the dynamics of the system and transforms a state (density matrix) $\rho$ into
another state $\mathcal{E}(\rho)$. Some special cases of QMCs have emerged,
such as open quantum walks [10] and classical-quantum (super-operator valued)
Markov chains [11], where the latter resemble classical Markov chains but with
the transition stochastic matrix $P=\\{p_{i,j}\\}_{i,j\in S}$ being replaced
by a transition set $\\{\mathcal{E}_{i,j}\\}_{i,j\in S}$ of super-operators,
while still maintaining the finite state set $S$.

Temporal Logics. The dynamic extension of Birkhoff–von Neumann quantum logic
[12] was proposed to specify a wide range of temporal properties of quantum
systems. In this approach, atomic propositions are used to describe
qualitative properties of a quantum system, represented as closed subspaces of
the system’s state Hilbert space (whether or not a quantum state $\rho$ is in
a subspace $\mathcal{X}$ of $\mathcal{H}$). Furthermore, QMCs are abstracted
as subspace transition systems, and the temporal properties of interest are
represented by infinite sequences of sets of atomic propositions (subspaces)
[3]. This subspace-based temporal logic allows for the specification of
linear-time properties, such as invariants and safety properties, for quantum
automata (a simplified form of QMCs) [13]. Model-checking algorithms have been
developed for the subspace-based temporal logic in [14], and the
(un)decidability of model checking quantum automata has been studied in [15].
However, a limitation of model checking QMCs against subspace-based temporal
logics is that it can only handle qualitative properties, which means that
only simple examples can be checked. Given that the power of quantum systems
lies in their probabilistic nature, it is crucial to be able to check
probabilistic (quantitative) properties.

To address this issue, in this paper we propose a measurement-based linear-
time temporal logic to capture these properties and develop a model-checking
algorithm to check the quantitative properties of QMCs. More specifically, we
observe that the properties of the quantum systems in question can be
described using quantum measurements, which extract classical (probabilistic)
information from quantum states. Building on this observation, we introduce
measurement-based atomic propositions to describe static quantitative
properties, namely, the measurement outcome probability of a quantum state
under a measurement. This can be seen as a generalization of the subspace-
based atomic propositions of the Birkhoff–von Neumann quantum logic [12],
where a quantum state $\rho$ in a subspace $\mathcal{X}\subseteq\mathcal{H}$
can be regarded as having a measurement outcome probability of $1$ under the
measurement onto $\mathcal{X}$. By combining with standard linear-time
temporal logic (LTL) [16, 1], we obtain MLTL, the measurement-based LTL, to
specify the temporal quantitative properties of quantum systems.

In order to develop an algorithm for model checking QMCs against MLTL
formulas, we extend the Thiagarajan’s approximate verification [17] of a
stochastic transition matrix $P$ to encompass more general linear operators in
quantum systems, e.g., the super-operators. The key technique for this
generalization is based on the eigenvalue analysis of QMCs, which simplifies
the previous work based on the _Bottom Strongly Connected Component (BSCC)
decomposition_ [1] of the state space of classical Markov chains [17].
Subsequently, we provide an effective procedure for the approximate model
checking of QMCs against MLTL formulas. In Section 6, we provide several case
studies to illustrate how our model and algorithm can be applied in a quantum
walk. These case studies help to verify the previously established advantages
of quantum walks over classical random walks, as discovered by Ambainis et al.
[18]. Additionally, we explore new phenomena unique to quantum walks when we
verify the same MLTL formulas on both types of walks.

In summary, this paper makes the following main contributions:

  1. 1.

_Introducing_ a quantum temporal logic, called measurement-based linear-time
logic (MLTL), which allows for specifying quantitative properties of QMCs.

  2. 2.

_Generalizing_ symbolic dynamics-based verification techniques of the
transition stochastic matrix given in [17] to more general quantum linear
operators (super-operators) by _eigenvalue analysis_ ; based on this, a model-
checking algorithm for QMCs against MLTL is developed.

  3. 3.

_Verifying_ numerous quantitative properties of quantum walks through our
model-checking algorithm as case studies. This serves to validate the
established advantages of quantum walks over their classical counterparts and
discover new phenomena unique to quantum walks.

###  1.1 Related Works and Challenges

To provide a suitable context for our work, let us delve deeper into the
discussion of related works and the challenges we encounter in this paper.

Hybrid vs. Quantum Temporal Logic. In a previous study [11], a specialized
type of quantum Markov chain known as super-operator-valued quantum Markov
chain was proposed. This model was designed for the purpose of modeling
quantum programs and quantum cryptographic protocols. Additionally, a quantum
extension of the probabilistic computation tree logic (PCTL) called quantum
computation tree logic (QCTL) was introduced, along with a model-checking
algorithm specifically tailored for this Markov model.

However, these hybrid temporal logic approaches heavily rely on the classical
state graph and are not applicable to quantum systems. This is because quantum
systems have a continuous state space and an infinite number of states, making
it impossible to obtain a connection graph. In order to address this
limitation and specify the properties of quantum Markov chains, we propose a
measurement-based linear-time temporal logic (MLTL) approach that does not
require a connection graph. This allows us to directly reason about the
transitions of measurement outcome probability distributions. Our MLTL
approach adopts classical LTL with quantum physical interpretation, providing
the advantage of utilizing existing classical techniques and facilitating
contributions from the classical model-checking community to the field of
quantum computing.

Classical vs. Quantum Markov Chains. The main technique used for model
checking classical Markov chains in [17] involves studying the periodicity of
states in sub-chains obtained through BSCC decomposition [1], a widely-used
method in the field of model checking Markov chains. However, when it comes to
the quantum extension of this decomposition, as described in [19], the BSCC
decomposition of QMCs is not unique but there are infinitely many
decompositions due to the continuous state space, unlike the classical case.
Consequently, we cannot directly generalize Thiagarajan’s _approximate
verification_ [17]. To overcome this unique challenge posed by quantum
mechanics, we propose a method based on eigenvalue analysis to directly
explore the periodic properties of QMCs. As a result, QMCs are not always
periodically stable like classical Markov chains. We provide a way to
determine the periodic stability depending on the initial states of QMCs. With
these efforts, we successfully extend the idea of approximate model checking
to work for QMCs, pushing the application boundary of such model-checking
techniques to more general linear systems.

Model Checking Quantum Walks. As a result of the phenomenon known as _quantum
interference_ [20], quantum walks can propagate at significantly faster or
slower rates compared to their classical counterparts [18]. Quantum walks have
gained attention due to their potential application in the development of
randomized algorithms, with various quantum algorithms incorporating this
concept [8, 9]. Notably, in certain search problems, quantum walks can offer
quadratic or exponential speedups compared to classical algorithms.

Previously, researchers have conducted case-by-case studies on the dynamic
properties of quantum walks, requiring the introduction of various techniques
depending on the specific property and underlying topological structure of the
walks. In this paper, we introduce a model-checking method that overcomes this
limitation by allowing for the automatic verification of a wide range of
properties of the walks. To model quantum walks, we utilize QMCs, and to
specify the relevant dynamical properties, we employ MLTL formulas. By
simultaneously verifying classical and quantum walks using our model-checking
algorithm, we can confirm the advantages of quantum walks that have already
been established in [18], as well as discover new phenomena that are distinct
from classical random walks. We anticipate that these new phenomena,
discovered by our model-checking algorithm, will contribute to the development
of more efficient quantum walk-based algorithms with enhanced speedup
capabilities.

##  2 Preliminaries

In this section, we aim to explain the three components that appear in a QMC
$\mathcal{Q}=(\mathcal{H},\mathcal{E},\rho_{0})$, as well as quantum
measurements, an essential part of our MLTL.

Quantum State Space $\mathcal{H}$. The _state space_ of a quantum system is a
finite-dimensional linear space $\mathcal{H}$, which is commonly known as the
_Hilbert space_ in the field of quantum computing. A _quantum pure state_ is
represented by a unit complex column vector $\psi$ in $\mathcal{H}$. In the
field of quantum computing, the _bra-ket notation_ is widely used to represent
quantum states, making it easier to perform calculations that frequently arise
in quantum mechanics. This notation uses angle brackets, $\langle$ and
$\rangle$, along with a vertical bar $|$, to construct “bras” and “kets” that
represent row and column vectors, respectively. The following list provides
the notation used in this paper to represent linear algebra concepts:

  1. 1.

$|\psi\rangle$ represents a unit complex column vector (quantum pure state) in
$\mathcal{H}$, labeled with $\psi$;

  2. 2.

$\langle\psi|:=|\psi\rangle^{\dagger}$ denotes the complex conjugate and
transpose of $|\psi\rangle$;

  3. 3.

$\langle\psi_{1}|\psi_{2}\rangle:=\langle\psi_{1}||\psi_{2}\rangle$ represents
the inner product of $|\psi_{1}\rangle$ and $|\psi_{2}\rangle$;

  4. 4.

$|\psi_{1}\rangle\langle\psi_{2}|:=|\psi_{1}\rangle\cdot\langle\psi_{2}|$
denotes the outer product of $|\psi_{1}\rangle$ and $|\psi_{2}\rangle$.

It is important to note that any vector in $\mathcal{H}$ can be linearly
represented by a _computational basis_ , which is a set of mutually orthogonal
unit vectors. In order to compare with classical Markov chains denoted as
$(S,P,\mu_{0})$, we use the finite state set $S=\\{s_{0},\dotsc,s_{d-1}\\}$ to
label the computational basis of $\mathcal{H}$, with dimension $d$, as
$\\{|s_{0}\rangle,\dotsc,|s_{d-1}\rangle\\}$. Here, $|s_{k}\rangle$ is a unit
column vector with the $k$-th element being $1$ and the remaining elements
being $0$ (the index starts from $0$). Then $\mathcal{H}$ is denoted as
$\mathcal{H}=\operatorname{span}\\{|s_{0}\rangle,\dotsc,|s_{d-1}\rangle\\}$.

Using this basis, any quantum state $|\psi\rangle$ in $\mathcal{H}$ can be
expressed as a linear combination of
$\\{|s_{0}\rangle,\dotsc,|s_{d-1}\rangle\\}$ with complex coefficients
$a_{k}$: $|\psi\rangle=\sum_{k=0}^{d-1}a_{k}|s_{k}\rangle$ with the
normalization condition
$\langle\psi|\psi\rangle=\sum_{k=0}^{d-1}a_{k}a_{k}^{*}=1$, where $a_{k}^{*}$
is the complex conjugate of $a_{k}$. In the case of a $2$-dimensional space,
we have:

$|s_{0}\rangle=\left(\begin{matrix}1\\\
0\end{matrix}\right)\qquad|s_{1}\rangle=\left(\begin{matrix}0\\\
1\end{matrix}\right)\qquad|\psi\rangle=\left(\begin{matrix}a_{0}\\\
a_{1}\end{matrix}\right)\qquad\langle\psi|=\left(\begin{matrix}a_{0}^{*},a_{1}^{*}\end{matrix}\right).$

It is evident that a quantum pure state has the capability to depict a
_superposition_ of state set $S=\\{s_{0},\ldots,s_{d-1}\\}$ as
$|\psi\rangle=\sum_{k=0}^{d-1}a_{k}|s_{k}\rangle$. The superposition is a
unique feature of quantum systems and the main reason for the advantages of
quantum algorithms over their classical counterparts [21].

Quantum Mixed State $\rho$. In quantum mechanics, uncertainty is a common
characteristic of quantum systems, arising from quantum noise and
measurements. To describe the uncertainty of possible quantum pure states, the
concept of _quantum mixed state_ $\rho$ on $\mathcal{H}$ is introduced. It can
be represented as

$\displaystyle\rho=\sum_{k}p_{k}|\psi_{k}\rangle\langle\psi_{k}|.$ (1)

Here, $\\{(p_{k},|\psi_{k}\rangle)\\}_{k}$ represents an ensemble, indicating
that the quantum state is at $|\psi_{k}\rangle$ with probability $p_{k}$. This
concept can also be used to describe the uncertainty of a classical
probability distribution, where each $|\psi_{k}\rangle$ represents $s_{k}$ by
$|\psi_{k}\rangle=|s_{k}\rangle$. Specifically, a (row) probability
distribution $\mu=(p_{0},\dotsc,p_{d-1})$ over the state set
$S=\\{s_{0},\dotsc,s_{d-1}\\}$ can be represented by a quantum mixed state.
This representation involves a diagonal matrix on $\mathcal{H}$, where the
diagonal elements correspond to the probabilities $p_{k}$ as follows.

$\displaystyle\rho_{\mu}=\sum_{k}p_{k}|s_{k}\rangle\langle
s_{k}|=\mathrm{diag}(p_{0},\ldots,p_{d-1}).$ (2)

Hence, a quantum mixed state $\rho$ is an extension of a probability
distribution $\mu$. Generally, the quantum uncertainty is more complex because
the ensemble decomposition in Eq. (1) of a quantum state $\rho$ can have
infinitely many variants. This means that $\rho$ can represent multiple
ensembles $\\{(p_{k},|\psi_{k}\rangle)\\}_{k}$ simultaneously.

From a mathematical perspective, a quantum mixed state $\rho\in\mathcal{L(H)}$
is a linear operator ($d$-by-$d$ matrix) on $\mathcal{H}$ that satisfies three
conditions: 1) _Hermitian_ $\rho^{\dagger}=\rho$; 2) _positive semi-definite_
$\langle\psi|\rho|\psi\rangle\geq 0$ for all $|\psi\rangle\in\mathcal{H}$; and
3) _unit trace_ ${\rm tr}(\rho)=\sum_{k}\langle s_{k}|\rho|s_{k}\rangle=1$,
where ${\rm tr}(\rho)$ is the trace of $\rho$ and represents the sum of the
diagonal elements of $\rho$. Here, $\mathcal{L(H)}$ denotes the set of linear
operators on $\mathcal{H}$. Let $\mathcal{D(H)}\subseteq\mathcal{L(H)}$ be the
set of all quantum mixed states on $\mathcal{H}$. To avoid any ambiguity, in
the subsequent discussion, the term “quantum states” will specifically refer
to quantum mixed states, given that we are considering the broader scenario.

Quantum Evolution $\mathcal{E}$. In the realm of quantum computing, the
evolution of a quantum system is commonly represented by the equation

$\rho^{\prime}=\mathcal{E}(\rho).$ (3)

Here, $\mathcal{E}$ is referred to as a _super-operator_. Mathematically,
$\mathcal{E}(\,\mathord{\cdot}\,)$ is a linear mapping from $\mathcal{L(H)}$
to $\mathcal{L(H)}$, allowing for the transformation of one quantum state
$\rho$ into another $\rho^{\prime}$. As stated by the _Kraus representation
theorem_ [22], $\mathcal{E}$ can be characterized by a finite set of
$d$-by-$d$ matrices $\\{\,E_{k}:0\leq k\leq m-1\,\\}\subseteq\mathcal{L(H)}$,
where $m\leq d^{2}$. The expression is given by
$\mathcal{E}(\rho)=\sum_{k=0}^{m-1}E_{k}\rho E_{k}^{{\dagger}}$ for all
$\rho\in\mathcal{D(H)}$.

This representation also satisfies the trace-preserving condition
$\sum_{k}E_{k}^{{\dagger}}E_{k}=I$, where $I$ is the identity matrix on
$\mathcal{H}$ and ${\dagger}$ denotes the complex conjugate and transpose of
matrices. In other words, for all $\rho\in\mathcal{D(H)}$, we have ${\rm
tr}(\mathcal{E}(\rho))={\rm tr}(\rho)$ by ${\rm tr}(\mathcal{E}(\rho))={\rm
tr}(\sum_{k}E_{k}\rho E_{k}^{\dagger})={\rm
tr}(\sum_{k}E_{k}^{\dagger}E_{k}\rho)={\rm tr}(\rho).$

An example of the use of super-operators can be found in Section 3.1, where a
super-operator is employed to represent the evolution of quantum walks. In the
degenerate scenario, the Kraus operator is simplified to only include a
_unitary matrix_ $U$ on $\mathcal{H}$ (where $U^{\dagger}U=U^{\dagger}U=I$),
and $\mathcal{E}(\rho)=U\rho U^{\dagger}$.

Quantum Measurement. To extract information from a quantum state, a _quantum
measurement_ is performed. This measurement yields a classical outcome which
is represented as a probability distribution over the possible results.
Mathematically, a quantum measurement is described by a set
$\\{M_{k}\\}_{k\in\mathcal{O}}$ of positive semi-definite matrices on the
state (Hilbert) space $\mathcal{H}$, where $\mathcal{O}$ is a finite set of
possible outcomes. The measurement process is probabilistic: if the quantum
system is in a state $\rho$ before the measurement, the probability of
obtaining the outcome $k$ is given as follows.

$p_{k}={\rm tr}(M_{k}\rho).$

Note that the measurement $\\{M_{k}\\}_{k\in\mathcal{O}}$ satisfies the _unity
condition_ $\sum_{k}M_{k}=I$, which guarantees that the total probability of
all outcomes is equal to $1$. In other words, $\sum_{k}{\rm
tr}(M_{k}\rho)={\rm tr}(\sum_{k}M_{k}\rho)={\rm tr}(\rho)=1$.

In the case where we want to extract the classical probability distribution
$\mu$ encoded in the quantum state $\rho_{\mu}$ as shown in Eq. (2), we can
choose the measurement $\\{M_{k}=|s_{k}\rangle\langle s_{k}|\\}_{s_{k}\in S}$.
In this scenario, the measurement probability of obtaining outcome $s_{k}$ is
given by

${\rm tr}(|s_{k}\rangle\langle s_{k}|\rho_{\mu})=\sum_{l}\langle
s_{l}||s_{k}\rangle\langle s_{k}|\rho_{\mu}|s_{l}\rangle=\langle
s_{k}|\rho_{\mu}|s_{k}\rangle=\langle s_{k}|(\sum_{j}p_{j}|s_{j}\rangle\langle
s_{j}|)|s_{k}\rangle=p_{k}.$

The above equations rely on the mutual orthogonality of the computational
basis $\\{|s_{0}\rangle,\dotsc,|s_{d-1}\rangle\\}$, meaning that $\langle
s_{j}|s_{l}\rangle=0$ for $j\neq l$, and also the fact that each
$|s_{k}\rangle$ is normalized, represented by $\langle s_{k}|s_{k}\rangle=1$.

It should be noted that after the measurement, the state will collapse or be
altered, depending on the measurement outcome $k$, which distinguishes quantum
computation from classical computation. For instance, in the case of a
_projection measurement_ denoted as $\\{P_{k}\\}_{k\in\mathcal{O}}$, the state
after obtaining outcome $k$ is given by $P_{k}\rho P_{k}/p_{k}$ with
$p_{k}={\rm tr}(P_{k}\rho)$. Here, each positive semi-definite matrix $P_{k}$
represents a projection operator ($P_{k}^{2}=P_{k}$), and a specific example
of a projection measurement is the above measurement $\\{|s_{k}\rangle\langle
s_{k}|\\}_{s_{k}\in S}$. Another concrete example is provided in Example 2 for
the case of quantum walks. For other scenarios involving post-measurement
states that are not encountered in this paper, please refer to [21, Section
2.2.3].

##  3 Quantum Markov Chains

In this section, we present the formal definition of QMCs. For a more detailed
discussion, we refer the interested readers to [3].

###### Definition 1

A QMC is a tuple $\mathcal{G}=(\mathcal{H},\mathcal{E},\rho_{0})$, where
$\mathcal{H}$ is a finite-dimensional Hilbert space, $\mathcal{E}$ is a super-
operator on $\mathcal{H}$, and $\rho_{0}\in\mathcal{D(H)}$ is an initial
state.

The execution of $\mathcal{G}$ is naturally described by the trajectory of
quantum states:

$\sigma(\mathcal{G}):=\rho_{0},\mathcal{E}(\rho_{0}),\mathcal{E}^{2}(\rho_{0}),\ldots.$
(4)

QMCs are a direct extension of classical Markov chains and can simulate their
execution; see the following example.

######  Example 1 (Classical Markov chains as QMCs)

Not surprisingly, any classical Markov chain $(S,P,\mu_{0})$ can be
effectively encoded as a QMC. We can use
$\mathcal{H}=\operatorname{span}\\{|s_{0}\rangle,\dotsc,|s_{d-1}\rangle\\}$ to
encode $S$, and $\mathcal{E}$ can be a super-operator with Kraus operators
$\\{E_{k,l}=\sqrt{p_{k,l}}|s_{l}\rangle\langle s_{k}|\\}_{s_{k},s_{l}\in S}$
that encode the probabilities $p_{k,l}$ of $P$.

It can be easily verified that $\mathcal{E}$ is a valid super-operator, i.e.,
$\sum_{k,l}E_{k,l}^{\dagger}E_{k,l}=I$. Furthermore, let $\rho_{0}=\sum_{s\in
S}\mu_{0}(s)|s\rangle\langle s|$ encode the initial probability distribution
$\mu_{0}$. Then, the QMC $(\mathcal{H},\mathcal{E},\rho_{0})$ can fully
simulate the behavior of $(S,P,\mu_{0})$ in the sense that for all $n\geq 0$:

$\mathcal{E}^{n}(\rho_{0})=\sum_{k=0}^{d-1}\mu_{n}(s_{k})|s_{k}\rangle\langle
s_{k}|=(\mu_{n}(s_{0}),\dotsc,\mu_{n}(s_{d-1})).$

Here, $\mu_{n}=\mu_{0}P^{n}$, $\mu_{n}(s_{k})$ represents the $k$-th entry of
$\mu_{n}$, and $\mathcal{E}^{0}=\operatorname{id}_{\mathcal{H}}$, which is the
_identity super-operator_ with only one Kraus operator $\\{I\\}$. The proof
follows a straightforward induction on $n$.

###  3.1 Quantum Walks

The case study of this paper is to explore the new and advanced properties of
quantum walks compared to classical random walks by model checking QMCs. This
exploration begins with modeling quantum walks using QMCs. Before presenting
this, we introduce one-dimensional quantum walks with absorbing boundaries in
the following example. Furthermore, we also need the bra-ket notation
$|\psi_{1}\rangle|\psi_{2}\rangle:=|\psi_{1}\rangle\otimes|\psi_{2}\rangle\in\mathcal{H}_{1}\otimes\mathcal{H}_{2}$,
which represents the composition (tensor product) of $|\psi_{1}\rangle$ and
$|\psi_{2}\rangle$ in the Hilbert spaces $\mathcal{H}_{1}$ and
$\mathcal{H}_{2}$, respectively.

######  Example 2 (Quantum walk with absorbing boundaries)

We consider an unbiased quantum walk on a one-dimensional lattice indexed from
$s_{0}$ to $s_{d}$, with the boundaries $s_{0}$ and $s_{d}$ being absorbing.

State Space. Let
$\mathcal{H}_{p}=\operatorname{span}\\{|s_{0}\rangle,\dotsc,|s_{d}\rangle\\}$
be a $(d+1)$-dimensional Hilbert space, where the pure state (unit vector)
$|s_{k}\rangle$ represents the position $s_{k}$ for each $0\leq k\leq d$. In
order to facilitate the evolution of the quantum walk, an additional coin
space is required. Let $\mathcal{H}_{c}$ be the coin (direction) space, which
is a $2$-dimensional Hilbert space with orthonormal basis states $|L\rangle$
and $|R\rangle$, indicating the directions left and right, respectively.
Therefore, the state space of the quantum walk is
$\mathcal{H}=\mathcal{H}_{p}\otimes\mathcal{H}_{c}$.

Initial State. The initial state is
$\rho_{0}=|\psi_{0}\rangle\langle\psi_{0}|$ with
$|\psi_{0}\rangle=|s_{k}\rangle|X\rangle$, indicating the initial position
$s_{k}$ and direction $X$, where $0\leq k\leq d$ and $X\in\\{L,R\\}$.

Evolution. Each step of the walk consists of three operations:

First, measure the current position of the system to determine whether it is
absorbing positions $s_{0}$ or $s_{d}$. If the position is $s_{0}$ or $s_{d}$,
then the walk terminates. The measurement is described by

$\\{M_{\mathit{yes}}=(|s_{0}\rangle\langle s_{0}|+|s_{n}\rangle\langle
s_{n}|)\otimes I_{c},M_{\mathit{no}}=I-M_{\mathit{yes}}\\}.$

Here, $I_{c}$ and $I$ are the identity operators on $\mathcal{H}_{c}$ and
$\mathcal{H}$, respectively. According to the principles of measurements, from
the current state $\rho$, the walk terminates at state $\rho_{\mathit{yes}}$
with probability $p_{\mathit{yes}}$, and it continues with state
$\rho_{\mathit{no}}$, with probability $p_{\mathit{no}}$, where

$p_{\mathit{x}}={\rm tr}(M_{\mathit{x}}\rho)\quad\text{ and
}\quad\rho_{\mathit{x}}={M_{\mathit{x}}\rho
M_{\mathit{x}}^{\dagger}}/p_{\mathit{x}}\quad\text{ for
}\quad\mathit{x}=\mathit{yes},\mathit{no}.$

Second, apply an unbiased “coin-tossing” (unitary) operator on the coin space
$\mathcal{H}_{c}$. This operator, denoted as $U_{H}$, is given by:

$U_{H}=\frac{1}{\sqrt{2}}\left(\begin{matrix}1&1\\\
1&-1\end{matrix}\right)=|+\rangle\langle L|+|-\rangle\langle R|.$

Here, $|\pm\rangle=\frac{1}{\sqrt{2}}(|L\rangle\pm|R\rangle)$. The operator
$U_{H}$ represents the _Hadamard operator_ on $\mathcal{H}_{c}$, where the
probabilities of going left and right are both equal to $0.5$.

Third, perform a shift (unitary) operator on the space $\mathcal{H}$. The
shift operator, denoted as $U_{S}$, is given by:

$U_{S}=\sum_{k=0}^{d}|s_{k\ominus 1}\rangle\langle
s_{k}|\otimes|L\rangle\langle L|+|s_{k\oplus 1}\rangle\langle
s_{k}|\otimes|R\rangle\langle R|.$

The intuitive meaning of the operator $U_{S}$ is that the system walks one
step left or right based on the coin state on $\mathcal{H}_{c}$. Here,
$\oplus$ and $\ominus$ represent addition and subtraction modulo $d+1$,
respectively.

In summary, in each step, given the current state $\rho$ as the input, the
quantum walk transforms $\rho$ into $\rho^{\prime}=U\rho_{no}U^{\dagger}$ with
a probability $p_{no}$, where $U=U_{S}(I_{p}\otimes U_{H})$ and $I_{p}$ is the
identity operator on $\mathcal{H}_{p}$. Additionally, the walk terminates at
state $\rho_{yes}$ with a probability $p_{yes}$. The resulting state
$\rho^{\prime}$ then serves as the input state for the subsequent step of the
quantum walk.

For a better understanding, Appendix 0.A provides a visual representation
(Fig. 1) that showcases the evolution of the quantum walk in Example 2 from a
physical perspective.

Now, we demonstrate how to represent the quantum walk given in Example 2 using
a QMC. To begin, we introduce the super-operator $\mathcal{E}$, which
incorporates the unitary operator $U$ representing the combined evolution of
the second and third operations of the quantum walk. For any given
$\rho\in\mathcal{D(H)}$, we let $\mathcal{E}(\rho)$ be

$\mathcal{E}(\rho)=UM_{\mathit{no}}\rho
M_{\mathit{no}}^{\dagger}U^{\dagger}+M_{\mathit{yes}}\rho
M_{\mathit{yes}}^{\dagger}.$

It is worth noting that $M_{\mathit{no}}M_{\mathit{yes}}=0$ and
$M_{\mathit{yes}}^{2}=M_{\mathit{yes}}$, indicating that once the QMC
terminates, its state remains unchanged. By using induction on the number of
steps, we can easily verify that the evolution of the quantum walk can be
modeled by the QMC
$(\mathcal{H}_{p}\otimes\mathcal{H}_{c},\mathcal{E},\rho_{0}=|\psi_{0}\rangle\langle\psi_{0}|)$.

##  4 Measurement-based Linear-time Temporal Logic

In this section, we introduce a specification language called _Measurement-
based Linear-time Temporal Logic_ (MLTL) for describing the properties of
quantum systems. MLTL is similar to ordinary LTL, but its atomic propositions
are interpreted in the context of quantum computing. It also expands on the
subspace-based atomic propositions introduced by Birkhoff and von Neumann
[12].

###  4.1 Measurement-based Atomic Propositions

As mentioned in Section 2, a quantum measurement is the process of extracting
classical information from quantum states. A quantum measurement can be
represented by a finite set $\\{M_{k}\\}_{k\in\mathcal{O}}$ of positive semi-
definite matrices with the unity condition $\sum_{k}M_{k}=I$. Each matrix
$M_{k}$ is called a _measurement operator_ and it is associated with the
probability ${\rm tr}(M_{k}\rho)$ of obtaining the outcome $k$ when measuring
the quantum state $\rho$. Mathematically, a measurement operator $M$ is
positive semi-definite and satisfies $M\leq I$, which means that $I-M$ is also
positive semi-definite.

In the following discussion, our main focus is on the measurement operator
$M_{k}$ and its associated probability ${\rm tr}(M_{k}\rho)$. Therefore, we
will often disregard the specific outcome value $k$ and simply refer to the
measurement operator as $M$. Additionally, we will not explicitly mention the
measurement consisting of $M$, as a binary quantum measurement $\\{M,I-M\\}$
can be determined based on $M$ itself (as seen in Example 2 with the
measurement operators $M_{\mathit{yes}}$ and $M_{\mathit{no}}$).

Our atomic propositions are designed to estimate the probability of the
outcome ${\rm tr}(M\rho)$ after measuring the quantum state $\rho$, given the
measurement operator $M$.

###### Definition 2

Given a Hilbert space $\mathcal{H}$,

  1. 1.

an atomic proposition in $\mathcal{H}$ is a pair $\langle
M,\mathcal{I}\rangle$, where $M$ represents a measurement operator on
$\mathcal{H}$ and $\mathcal{I}\subseteq[0,1]$ is an interval;

  2. 2.

a state $\rho\in\mathcal{D(H)}$ satisfies $\langle M,\mathcal{I}\rangle$,
written $\rho\models\langle M,\mathcal{I}\rangle$, if the outcome probability
of the measurement operator $M$ applied to $\rho$ falls within the interval
$\mathcal{I}$, that is, ${\rm tr}(M\rho)\in\mathcal{I}$.

In terms of the expressive power of our measurement-based atomic propositions,
it is worth noting that they extend the existing atomic propositions in both
the classical and quantum domains.

Classical:

the atomic proposition $\langle M,\mathcal{I}\rangle$ of $\rho$ expands upon
the proposition $\langle s_{k},\mathcal{I}\rangle$ of $\mu$ in interval
linear-time temporal logic. This classical logic has been used to specify
(static) properties of classical Markov chains [17] and continuous-time Markov
chains [23]. The proposition asserts that the probability of state $s_{k}\in
S$ in distribution $\mu$ over $S$ falls within the interval $\mathcal{I}$. The
extension is achieved by utilizing
$\rho_{\mu}=\sum_{k}\mu(s_{k})|s_{k}\rangle\langle s_{k}|$ in Eq. (2) and
$M=|s_{k}\rangle\langle s_{k}|$, resulting in ${\rm
tr}(M\rho_{\mu})=\mu(s_{k})$. Consequently, ${\rm
tr}(M\rho_{\mu})\in\mathcal{I}$ if and only if $\mu(s_{k})\in\mathcal{I}$.

Quantum:

furthermore, an atomic proposition $\langle M,\mathcal{I}\rangle$ of a mixed
state $\rho$ can encode the subspace-based proposition
$\mathcal{X}\subseteq\mathcal{H}$ of a pure state $|\psi\rangle$ in the
Birkhoff–von Neumann quantum logic. This proposition asserts that
$|\psi\rangle\in\mathcal{X}$. This observation is made by setting
$M=P_{\mathcal{X}}$, which represents the projection onto $\mathcal{X}$,
$\mathcal{I}=[1,1]$, and $\rho=|\psi\rangle\langle\psi|$. As a result, we can
conclude that $\rho=|\psi\rangle\langle\psi|\models\langle
P_{\mathcal{X}},[1,1]\rangle$ (i.e., ${\rm tr}(P_{\mathcal{X}}\rho)=1$) is
equivalent to $|\psi\rangle\in\mathcal{X}$.

To demonstrate the practicality of our atomic propositions, we will present a
series of specific instances in Example 3 later. These examples will
effectively illustrate the characteristics and properties of quantum walks.

From an algorithmic perspective, we gather a finite number of pairs $\langle
M,\mathcal{I}\rangle$ as the set of atomic propositions that are based on
quantum measurements. This set is denoted as $AP$.

###  4.2 Quantum Linear-Time Temporal Logic

In this section, we enhance the linear-time temporal logic [16, 1] by
incorporating the newly introduced measurement-based atomic propositions. This
will result in the formation of our measurement-based linear-time temporal
logic MLTL.

The MLTL formulas, which involve the use of measurement-based $AP$, are
defined according to the following syntax:

$\varphi::=\mathbf{true}\mid
a\mid\neg\varphi\mid\varphi_{1}\lor\varphi_{2}\mid\bigcirc\varphi\mid\varphi_{1}U\varphi_{2},$

where $a=\langle M,\mathcal{I}\rangle\in AP$. We can also derive additional
standard Boolean operators and temporal modalities such as $\lozenge$
(_eventually_) and $\square$ (_always_) using conventional methods.

The semantics of MLTL is also defined in a familiar manner. For any infinite
word $\xi$ over $2^{AP}$ and any MLTL formula $\varphi$ over $AP$, the
satisfaction relation $\xi\models\varphi$ is defined by induction on the
structure of $\varphi$:

  * •

$\xi\models\mathbf{true}$ always holds;

  * •

$\xi\models a$ iff $a\in\xi[0]$;

  * •

$\xi\models\neg\varphi$ iff it is not the case that $\xi\models\varphi$
(written $\xi\not\models\varphi$);

  * •

$\xi\models\varphi_{1}\lor\varphi_{2}$ iff $\xi\models\varphi_{1}$ or
$\xi\models\varphi_{2}$;

  * •

$\xi\models\bigcirc\varphi$ iff $\xi[1+]\models\varphi$; and

  * •

$\xi\models\varphi_{1}U\varphi_{2}$ iff there exists $k\geq 0$ such that
$\xi[k+]\models\varphi_{2}$ and for each $0\leq j<k$,
$\xi[j+]\models\varphi_{1}$,

where $\xi[k]$ and $\xi[k+]$ denote the $(k+1)$-th element and the $(k+1)$-th
suffix of $\xi$, respectively. The indexes start from zero so that, say,
$\xi=\xi[0+]$. In addition, the _semantics_ $\mathcal{L}_{\omega}(\varphi)$ of
$\varphi$ is defined as the language containing all infinite words over
$2^{AP}$ that satisfy $\varphi$:
$\mathcal{L}_{\omega}(\varphi)=\\{\,\xi\in(2^{AP})^{\omega}:\xi\models\varphi\,\\}.$

Now, let us extend the satisfaction relation $\rho\models a$ to
$\mathcal{G}\models\varphi$ between a QMC $\mathcal{G}$ and an MLTL formula
$\varphi$. To this end, we introduce the labeling function:

$L\colon\mathcal{D(H)}\to 2^{AP},\qquad L(\rho)=\\{\,a\in AP:\rho\models
a\,\\}$ (5)

which assigns to each quantum state $\rho$ the set of atomic propositions in
$AP$ satisfied by $\rho$. We further extend the labeling function to sequences
of quantum states by setting
$L(\rho_{0},\rho_{1},\ldots)=L(\rho_{0}),L(\rho_{1}),\ldots$ as usual. Then we
define:

$\mathcal{G}\models\varphi$ if and only if
$L(\sigma(\mathcal{G}))\in\mathcal{L}_{\omega}(\varphi)$

where $\sigma(\mathcal{G})$ is the state trajectory of $\mathcal{G}$ as
defined in Eq. (4).

We now exhibit realistic settings where our approach leads to valuable
insights for the quantum walk presented in Example 2.

######  Example 3 (Quantum walk with absorbing boundaries, continued)

Given a finite set of intervals
$\\{\mathcal{I}_{l}\subseteq[0,1]\\}_{l=0}^{L}$, let

$AP=\\{\,\langle
M_{s_{k}},\mathcal{I}_{l}\rangle:M_{s_{k}}=|s_{k}\rangle\langle s_{k}|\otimes
I_{c},0\leq k\leq d,0\leq l\leq L\,\\}$

with the atomic proposition $\langle M_{s_{k}},\mathcal{I}_{l}\rangle$
asserting that ${\rm tr}(M_{s_{k}}\rho)\in\mathcal{I}_{l}$ for $0\leq k\leq d$
and $0\leq l\leq L$. This allows us to trace the probability distribution on
all positions (including boundaries) of the quantum walk.

First, we can discuss the advantages of quantum walks over their classical
counterparts, as discovered by Ambainis et al. in [18]. When given the initial
state $|s_{1}\rangle|R\rangle$, the absorbing probability at position $0$
tends to $1/\sqrt{2}$ in the limit as $d\to\infty$, whereas in the classical
case, the value is $1$. This property can be expressed as the MLTL formula
$\varphi_{0}=\lozenge\square\langle M_{s_{0}},\mathcal{I}_{0}\rangle$, where
$\mathcal{I}_{0}=[1/\sqrt{2}-\gamma,1/\sqrt{2}+\gamma]$ and $\gamma>0$ is a
given precision parameter.

Next, we examine two properties of interest that demonstrate significant
differences between quantum walks and their classical counterparts. To the
best of our knowledge, these findings are new.

  1. 1.

In the classical case, the absorbing probability at position $d$ is always
smaller than 0.5 if the walk starts from the middle position and $d$ is even.
However, this does not necessarily hold for quantum walks. Let
$\varphi_{1}=\square\langle M_{s_{d}},\mathcal{I}_{1}\rangle$, where
$\mathcal{I}_{1}=[0,0.5)$, be the MLTL formula that expresses this property.
Assuming the initial state is $|s_{d/2}\rangle|R\rangle$, we will see in
Section 6 that $\varphi_{1}$ is false when $d=20$.

  2. 2.

Let $\mathcal{I}_{2}=(0.4,1]$ and $\varphi_{2}=\square(\langle
M_{s_{d-1}},\mathcal{I}_{2}\rangle\implies\langle
M_{s_{1}},\mathcal{I}_{2}\rangle)$, which states that at any given time point,
if the probability at position $d-1$ is larger than $0.4$, then the
probability at position $1$ is also larger than $0.4$. In the classical case,
$\varphi_{2}$ is true due to the symmetry of the distribution over positions.
However, as shown in Section 6, $\varphi_{2}$ does not hold in the quantum
case. Therefore, the distribution of the unbiased quantum walk over positions
is asymmetric even when the walk starts from the middle position.

##  5 Model Checking Algorithm

In this section, we present an algorithm that can be used to approximately
verify the satisfaction of $\mathcal{G}\models\varphi$. For the convenience of
the reader, we put all proofs of theoretical results in the appendix.

Using the notations in Eq. (5), we can formally define the model checking
problem for $\sigma(\mathcal{G})$ against MLTL formulas as follows.

###### Problem 1

Given a QMC $\mathcal{G}=(\mathcal{H},\mathcal{E},\rho_{0})$, a labeling
function $L$, and an MLTL formula $\varphi$, the task is to decide whether
$\mathcal{G}\models\varphi$, which means determining whether
$L(\sigma(\mathcal{G}))\in\mathcal{L}_{\omega}(\varphi)$.

Although MLTL extends LTL with quantum atomic propositions, the traditional
model-checking techniques for LTL cannot be directly applied to solve Problem
1. This is because the state space of a QMC is continuous and uncountably
infinite, even in the case where the state space is finite-dimensional. In
contrast, classical LTL model checking deals with a discrete and finite state
set. However, QMCs can simulate Markov chains as seen in Example 1, and
interval LTL formulas in [17] can be represented by MLTL formulas as discussed
in Section 4. Despite this, the counter-example presented in [17] shows that
the language $\\{L(\sigma(\mathcal{G}))\\}$ is generally not $\omega$-regular.
Therefore, the standard approach [24] of model checking $\omega$-regular
languages cannot directly solve Problem 1 either.

To address this, we turn to the problem of approximate verification for QMCs,
following the techniques introduced in [17]. The main idea in [17] involves
studying the periodicity of states in _finitely many_ sub-chains obtained
through BSCC decomposition [1], and a key property of Markov chains known as
_periodic stability_ , which ensures their stability. However, extending this
idea to the quantum setting is not straightforward. It has been proven that
the BSCC decomposition of QMCs is not unique, but rather has _infinitely many_
possibilities [19, 25, 26] due to the continuous state space. Additionally, we
will demonstrate below that QMCs do not exhibit periodic stability.

###### Definition 3

A QMC $\mathcal{G}=(\mathcal{H},\mathcal{E},\rho_{0})$ is called _periodically
stable_ if there exists an integer $\theta>0$ such that
$\lim_{n\to\infty}\mathcal{E}^{n\theta}(\rho_{0})=\rho^{*}$ for some limiting
quantum state $\rho^{*}$. The smallest value of $\theta$, if it exists, is
referred to as the _period_ of $\mathcal{G}$ and is denoted as
$p(\mathcal{G})$. Moreover, $\\{\,\mathcal{E}^{k}(\rho^{*}):0\leq
k<p(\mathcal{G})\,\\}$ are called the _periodically stable states_ of
$\mathcal{G}$ as
$\lim_{n\to\infty}\mathcal{E}^{n\theta}(\mathcal{E}^{k}(\rho_{0}))=\mathcal{E}^{k}(\rho^{*})$.

In the classical case, any Markov chain $(S,P,\mu_{0})$ is periodically stable
[27]. This means that there exists an integer $\theta>0$ such that
$\lim_{n\to\infty}\mu_{0}P^{n\theta}=\mu^{*}$ for some limiting distribution
$\mu^{*}$. Furthermore, $\theta$ is independent of $\mu_{0}$. However, this
property does not hold for QMCs, as demonstrated by the following example.

###### Example 4

Let $\mathcal{H}=\operatorname{span}\\{|s_{0}\rangle,|s_{1}\rangle\\}$ and
$U=|s_{0}\rangle\langle s_{0}|+e^{i2\pi\psi}|s_{1}\rangle\langle s_{1}|$ be a
unitary operator on $\mathcal{H}$, where $\psi$ is an irrational number. It
can be proven that the QMC $(\mathcal{H},\mathcal{E}_{U},\rho_{0})$, where
$\mathcal{E}_{U}(\rho)=U\rho U^{{\dagger}}$, is not periodically stable for
any generic initial state $\rho_{0}$. In fact, a simple calculation reveals
that

$\mathcal{E}_{U}^{n\theta}(\rho_{0})=\rho_{00}\cdot|s_{0}\rangle\langle
s_{0}|+\rho_{11}\cdot|s_{1}\rangle\langle s_{1}|+e^{-i2\pi\psi
n\theta}\rho_{01}\cdot|s_{0}\rangle\langle s_{1}|+e^{i2\pi\psi
n\theta}\rho_{10}\cdot|s_{1}\rangle\langle s_{0}|$

where $\rho_{ij}=\langle s_{i}|\rho|s_{j}\rangle$. It is worth noting that
since $\psi$ is irrational, the set $\\{\,e^{i2\pi\psi m}:m\in\mathbb{N}\,\\}$
is dense in the unit circle [28]. Therefore, for any integer $\theta>0$, the
limit $\lim_{n\to\infty}\mathcal{E}_{U}^{n\theta}(\rho_{0})$ cannot exist,
except when $\rho_{01}=\rho_{10}=0$.

Note that the operator $\mathcal{E}_{U}$ in Example 4 has four eigenvalues
(with multiplicity taken into account): $1$, $1$, $e^{-i2\pi\psi}$, and
$e^{i2\pi\psi}$. The corresponding eigenvectors are $|s_{0}\rangle\langle
s_{0}|$, $|s_{1}\rangle\langle s_{1}|$, $|s_{0}\rangle\langle s_{1}|$, and
$|s_{1}\rangle\langle s_{0}|$, respectively. We have proven that the system
$(\mathcal{H},\mathcal{E}_{U},\rho_{0})$ is periodically stable if and only if
the initial state $\rho_{0}$ does not have any components in the directions of
$|s_{0}\rangle\langle s_{1}|$ and $|s_{1}\rangle\langle s_{0}|$.
Interestingly, this is precisely why a QMC cannot be periodically stable (see
Appendix 0.B). To put it in another way, a QMC is periodically stable only if
the initial quantum state does not contain any components in the directions
defined by the eigenvectors of the relevant super-operator (linear operator)
corresponding to eigenvalues of the form $e^{i2\pi\psi}$ where $\psi$ is an
irrational number. This result also offers an efficient method to verify the
periodic stability of a given QMC $\mathcal{G}$ (and determine the period
$p(\mathcal{G})$). Specifically, symbolic computation can be used to check
whether the eigenvalues of QMCs are irrational by analyzing their algebraic
representations and mathematical properties. Such a method can be utilized to
confirm the periodic stability of the quantum walk in Example 2. Therefore,
the approximate verification technique described in this paper can be applied
to the quantum walk.

###### Proposition 1

Given a QMC $\mathcal{G}=(\mathcal{H},\mathcal{E},\rho_{0})$ with
$\dim(\mathcal{H})=d$, there is a way to check whether $\mathcal{G}$ is
periodically stable with computational complexity $\mathcal{O}(d^{8})$. If it
is indeed stable, we can compute the period $p(\mathcal{G})$ with a complexity
of $\mathcal{O}(d^{8})$.

The evaluation process for periodic stability, as described in Proposition 1,
involves examining the eigenvalues and eigenvectors of the super-operator
$\mathcal{E}$. To calculate these eigenvalues and eigenvectors of
$\mathcal{E}$ with Kraus operators $\\{E_{k}\\}_{k}$, we can use the matrix
representation $\mathcal{M}_{\mathcal{E}}$ [29] of $\mathcal{E}$, given by
$\mathcal{M}_{\mathcal{E}}=\sum_{k}E_{k}\otimes E_{k}^{*}.$ Here, $E_{k}^{*}$
represents the entry-wise complex conjugate of $E_{k}$. The linear operator
(matrix) $\mathcal{M}_{\mathcal{E}}$ acts on $\mathcal{H}\otimes\mathcal{H}$.
Based on this, we can derive the following lemma:

###### Lemma 1

For a non-zero $A\in\mathcal{L(H)}$, $A$ is an eigenvector of $\mathcal{E}$
corresponding to the eigenvalue $\lambda$ if and only if $|A\rangle$ is an
eigenvector of $\mathcal{M}_{\mathcal{E}}$ corresponding to the eigenvalue
$\lambda$. In other words, $\mathcal{E}(A)=\lambda A$ if and only if
$\mathcal{M}_{\mathcal{E}}|A\rangle=\lambda|A\rangle$.

In this context, $|A\rangle\in\mathcal{H}\otimes\mathcal{H}$ represents the
vectorization of $A$, denoted by $|A\rangle:=(A\otimes I)|\Omega\rangle$.
Here, $|\Omega\rangle$ denotes the (unnormalized) maximally entangled state on
$\mathcal{H}\otimes\mathcal{H}$ [21]. Assuming
$\mathcal{H}=\operatorname{span}\\{|s_{0}\rangle,\dotsc,|s_{d-1}\rangle\\}$,
the maximally entangled state can be expressed as
$|\Omega\rangle=\sum_{k=0}^{d-1}|s_{k}\rangle|s_{k}\rangle$. In particular,
for a quantum state $\rho\in\mathcal{D(H)}$, we write
$|\rho\rangle=(\rho\otimes I)|\Omega\rangle$.

Now, our attention can be directed towards approximately model checking the
QMC $\mathcal{G}$ that is periodically stable. To achieve this with a desired
level of accuracy $\varepsilon$, we can adopt the following approach. First
and foremost, we need to identify the states of the chain that are
periodically stable as defined in Definition 3. After a sufficient number of
steps, any state on the trajectory $\sigma(\mathcal{G})$ will be close to one
of the periodically stable states. This approach can also be applied to the
labeled trajectory $L(\sigma(\mathcal{G}))$. By doing so, we can obtain an
$\omega$-regular language. Following that, we can utilize the standard Büchi
automata approach of model checking $\omega$-regular languages to analyze the
obtained language. Therefore, in the following subsections, we will outline
the step-by-step process for handling this.

###  5.1 Periodically Stable States

Given a periodically stable QMC $(\mathcal{H},\mathcal{E},\rho_{0})$, we can
obtain the periodically stable states by employing a specific super-operator
called the _stabilizer_ of $\mathcal{G}$, denoted by $\mathcal{E}_{\phi}$.
This stabilizer is generated by the super-operator $\mathcal{E}$.

###### Lemma 2

If a QMC $\mathcal{G}=(\mathcal{H},\mathcal{E},\rho_{0})$ is periodically
stable with period $p(\mathcal{G})$, then the set
$\\{\mathcal{E}_{\phi}(\mathcal{E}^{k}(\rho_{0}))\\}_{0\leq k<p(\mathcal{G})}$
consists of the periodically stable states of $\mathcal{G}$. The computational
complexity of obtaining such a set is $\mathcal{O}(d^{8})$, where
$d=\dim(\mathcal{H})$.

The super-operator $\mathcal{E}_{\phi}$ is constructed from $\mathcal{E}$ by
retaining the eigenvectors corresponding to eigenvalues with a magnitude of
one, which do not vanish in the evolution $\mathcal{E}^{n}(\rho)$ as $n$ tends
to infinity. Specifically, let $\mathcal{M}_{\mathcal{E}}$ be the matrix
representation of $\mathcal{E}$ with Jordan decomposition
$\mathcal{M}_{\mathcal{E}}=SJS^{-1}$, where
$J=\bigoplus_{k=0}^{K}J_{k}(\lambda_{k})=\bigoplus_{k=0}^{K}\lambda_{k}P_{k}+N_{k}$.
Here, $\lambda_{k}$ represents the eigenvalues of $\mathcal{M}_{\mathcal{E}}$,
$P_{k}$ is a projector onto the corresponding (generalized) eigenvector space,
and $N_{k}$ is the corresponding nilpotent part. Furthermore, according to [7,
Proposition 6.2], the geometric multiplicity of any $\lambda_{k}$ with a
magnitude of one (i.e., $|\lambda_{k}|=1$) is equal to its algebraic
multiplicity, i.e., $N_{k}=0$. Then we define
$J_{\phi}:=\bigoplus_{k:|\lambda_{k}|=1}P_{k}$ as the projector onto the
eigenspace corresponding to eigenvalues with magnitude one. By [7, Proposition
6.3], it is confirmed that $\mathcal{M}_{\mathcal{E}_{\phi}}=SJ_{\phi}S^{-1}$
is indeed the matrix representation of some super-operator
$\mathcal{E}_{\phi}$.

###  5.2 Neighborhood of Quantum States

Now we proceed to introduce the concepts of (symbolic) neighborhoods for
(sequences of) quantum states using the labeling function $L$.

###### Definition 4

Let $\rho\in\mathcal{D(H)}$ be a quantum state and $\varepsilon>0$. The
(symbolic) $\varepsilon$-neighborhood $\mathcal{N}_{\varepsilon}(\rho)$ of
$\rho$ is the subset of $2^{AP}$ defined as

$\mathcal{N}_{\varepsilon}(\rho):=\\{\,L(\rho^{\prime}):\rho^{\prime}\in\mathcal{D(H)},\|\rho-\rho^{\prime}\|<\varepsilon\,\\},$

where $\|A\|:=\sqrt{{\rm tr}(A^{\dagger}A)}$ represents the Schatten 2-norm
(also known as the Hilbert–Schmidt norm) for the linear operator
$A\in\mathcal{L(H)}$.

Now we show that, after a certain number of steps, the symbols
$L(\mathcal{E}^{n}(\rho_{0}))$ will be enclosed within the
$\varepsilon$-neighborhood of one of the periodically stable states.

###### Lemma 3

Consider a periodically stable QMC
$\mathcal{G}=(\mathcal{H},\mathcal{E},\rho_{0})$ with period $p(\mathcal{G})$.
Let $\eta_{k}=\mathcal{E}_{\phi}(\mathcal{E}^{k}(\rho_{0}))$, for each $0\leq
k<p(\mathcal{G})$, as the periodically stable states of $\mathcal{G}$. Then
for any $\varepsilon>0$, there exists an integer $K^{\varepsilon}>0$ such that
for any $n\geq K^{\varepsilon}$,

$L(\mathcal{E}^{n}(\rho_{0}))\in\mathcal{N}_{\varepsilon}(\eta_{n\operatorname{mod}p(\mathcal{G})}).$

Moreover, the time complexity of computing $K^{\varepsilon}$ is in
$\mathcal{O}(d^{8})$, where $d=\dim(\mathcal{H})$.

With Lemma 3, we can define the concept of the (symbolic) neighborhood of
trajectories for periodically stable QMCs.

###### Definition 5

Given a periodically stable QMC
$\mathcal{G}=(\mathcal{H},\mathcal{E},\rho_{0})$ and $\varepsilon>0$, the
(symbolic) $\varepsilon$-neighborhood of the trajectory $\sigma(\mathcal{G})$
of $\mathcal{G}$ is defined to be the language
$\mathcal{N}_{\varepsilon}(\sigma(\mathcal{G}))$ over $(2^{AP})^{\omega}$ such
that $\xi\in\mathcal{N}_{\varepsilon}(\sigma(\mathcal{G}))$ if and only if

  * •

$\xi[n]=L(\mathcal{E}^{n}(\rho_{0}))$ for all $0\leq n\leq K^{\varepsilon}-1$
and

  * •

$\xi[n]\in\mathcal{N}_{\varepsilon}(\eta_{n\operatorname{mod}p(\mathcal{G})})$
for all $n\geq K^{\varepsilon}$,

where the states $\\{\,\eta_{k}:0\leq k<p(\mathcal{G})\,\\}$ and
$K^{\varepsilon}$ are as given in Lemma 3.

###  5.3 Approximate Verification of Quantum Markov Chains

Using Definition 5, we can formulate and address the problem of approximate
model checking for QMCs against MLTL formulas in the following manner.

###### Problem 2

Given a periodically stable QMC
$\mathcal{G}=(\mathcal{H},\mathcal{E},\rho_{0})$, a labeling function $L$, an
MLTL formula $\varphi$, and $\varepsilon>0$, decide whether

  1. 1.

_$\mathcal{G}$ $\varepsilon$-approximately satisfies $\varphi$ from below_,
denoted $\mathcal{G}\models_{\varepsilon}\varphi$; that is, whether
$\mathcal{N}_{\varepsilon}(\sigma(\mathcal{G}))\cap\mathcal{L}_{\omega}(\varphi)\neq\emptyset$;

  2. 2.

_$\mathcal{G}$ $\varepsilon$-approximately satisfies $\varphi$ from above_,
denoted $\mathcal{G}\models^{\varepsilon}\varphi$; that is, whether
$\mathcal{N}_{\varepsilon}(\sigma(\mathcal{G}))\subseteq\mathcal{L}_{\omega}(\varphi)$.

To justify that Problem 2 is indeed an approximate version of Problem 1, we
first note that
$L(\sigma(\mathcal{G}))\in\mathcal{N}_{\varepsilon}(\sigma(\mathcal{G}))$.
Then we have three cases:

  1. 1.

if $\mathcal{G}\not\models_{\varepsilon}\varphi$, then
$\mathcal{N}_{\varepsilon}(\sigma(\mathcal{G}))\cap\mathcal{L}_{\omega}(\varphi)=\emptyset$,
and hence $L(\sigma(\mathcal{G}))\notin\mathcal{L}_{\omega}(\varphi)$
($\mathcal{G}\not\models\varphi$);

  2. 2.

if $\mathcal{G}\models^{\varepsilon}\varphi$, then
$\mathcal{N}_{\varepsilon}(\sigma(\mathcal{G}))\subseteq\mathcal{L}_{\omega}(\varphi)$,
and hence $L(\sigma(\mathcal{G}))\in\mathcal{L}_{\omega}(\varphi)$
($\mathcal{G}\models\varphi$);

  3. 3.

if neither $\mathcal{G}\not\models_{\varepsilon}\varphi$ nor
$\mathcal{G}\models^{\varepsilon}\varphi$, then whether or not
$\mathcal{G}\models\varphi$ is unknown.

If we find ourselves in the third scenario (the unknown case), we have the
option to decrease the value of $\varepsilon$ by half and then repeat the
approximate model-checking process described in the previous scenarios. We can
continue this process until we reach either of the first two cases, which will
provide us with either a negative or affirmative answer to Problem 1. In
exceptional cases, diminishing $\varepsilon$ may not lead to termination. To
prevent this, a predetermined number of iterations can be set for reducing
epsilon. Determining when the procedure terminates seems difficult, and we
would like to leave it as future work.

Finally, to solve Problem 2, we represent
$\mathcal{N}_{\varepsilon}(\sigma(\mathcal{G}))$ in Definition 5 as the
$\omega$-regular expression

$\mathcal{N}_{\varepsilon}(\sigma(\mathcal{G}))=\\{L(\rho_{0})\\}\cdot\\{L(\mathcal{E}(\rho_{0}))\\}\cdots\\{L(\mathcal{E}^{K^{\varepsilon}-1}(\rho_{0}))\\}\cdot\left(\mathcal{N}_{\varepsilon}(\zeta_{0})\cdots\mathcal{N}_{\varepsilon}(\zeta_{p(\mathcal{G})-1})\right)^{\omega}$

where $\zeta_{k}=\eta_{(K^{\varepsilon}+k)\operatorname{mod}p(\mathcal{G})}$,
$0\leq k<p(\mathcal{G})$, and for any two sets $X$ and $Y$, $X\cdot
Y=\\{\,xy:x\in X,y\in Y\,\\}$. Thus
$\mathcal{N}_{\varepsilon}(\sigma(\mathcal{G}))$ is $\omega$-regular and
standard techniques [1, 30] can be employed to check
$\mathcal{N}_{\varepsilon}(\sigma(\mathcal{G}))\cap\mathcal{L}_{\omega}(\varphi)=\emptyset$
and
$\mathcal{N}_{\varepsilon}(\sigma(\mathcal{G}))\subseteq\mathcal{L}_{\omega}(\varphi)$.

Algorithm 1 ModelCheck($\mathcal{G},AP,L,\varphi,\varepsilon$)

0: A periodically stable QMC $\mathcal{G}=(\mathcal{H},\mathcal{E},\rho_{0})$
with Kraus operators $\\{E_{k}\\}_{k}$, a finite set of (measurement-based)
atomic propositions $AP$, a labeling function $L$, an MLTL formula $\varphi$,
and $\varepsilon>0$.

0: true, false, or unknown, where true indicates $\mathcal{G}\models\varphi$,
false indicates $\mathcal{G}\not\models\varphi$, and unknown stands for an
inconclusive answer.

1: Put $\mathcal{M}_{\mathcal{E}}=\sum_{k}E_{k}\otimes E_{k}^{*}$

2: Get $p(\mathcal{G})$ and $M_{\mathcal{E}_{\phi}}=SJ_{\phi}S^{-1}$ by the
Jordan decomposition form $\mathcal{M}_{\mathcal{E}}=SJS^{-1}$

3: Put $|\rho_{0}\rangle=(\rho_{0}\otimes\mathcal{I})|\Omega\rangle$

4: for each $k\in\\{0,1,\dotsc,p(\mathcal{G})-1\\}$ do

5: Set $|\eta_{k}\rangle$ to be
$M_{\mathcal{E}_{\phi}}M^{k}_{\mathcal{E}}|\rho_{0}\rangle$

6: Compute $\mathcal{N}_{\varepsilon}(\eta_{k})$ by semi-definite programming

7: end for

8: Get $K^{\varepsilon}$ by solving some inequalities

9: for each $k\in\\{0,1,\dotsc,K^{\varepsilon}-1\\}$ do

10: Put $\rho_{k}=\mathcal{E}^{k}(\rho_{0})$ and compute $L(\rho_{k})$

11: end for

12: Put $\zeta_{k}=\eta_{(K^{\varepsilon}+k)\operatorname{mod}p(\mathcal{G})}$
for $0\leq k<p(\mathcal{G})$

13: Let $\mathcal{N}_{\varepsilon}(\sigma(\mathcal{G}))$ be the
$\omega$-regular language
$\\{L(\rho_{0})\\}\\{L(\rho_{1})\\}\cdots\\{L(\rho_{K^{\varepsilon}-1})\\}\cdot(\mathcal{N}_{\varepsilon}(\zeta_{0})\mathcal{N}_{\varepsilon}(\zeta_{1})\cdots\mathcal{N}_{\varepsilon}(\zeta_{p(\mathcal{G})-1}))^{\omega}$

14: Construct the NBA $A_{\varphi}$ for $\varphi$ // standard construction

15: Construct the NBA $A_{\mathcal{G}}$ accepting
$\mathcal{N}_{\varepsilon}(\sigma(\mathcal{G}))$// standard lasso-shaped
construction

16: if $\mathcal{L}(A_{\mathcal{G}})\cap\mathcal{L}(A_{\varphi})=\emptyset$
then // standard Büchi automata operation

17: return false

18: else if $\mathcal{L}(A_{\mathcal{G}})\subseteq\mathcal{L}(A_{\varphi})$
then // standard Büchi automata operation

19: return true

20: else

21: return unknown

22: end if

###### Theorem 5.1

The verification problem outlined in Problem 2 can be addressed using
Algorithm 1 within a time complexity of
$\mathcal{O}(2^{\mathcal{O}(|\varphi|)}\cdot(K^{\varepsilon}+p(\mathcal{G}))+d^{8})$.
Here, $d=\dim(\mathcal{H})$, $|\varphi|$ represents the size of MLTL formula
$\varphi$, and $p(\mathcal{G})$ and $K^{\varepsilon}$ are as given in
Proposition 1 and Lemma 3, respectively.

Algorithm 1 summarizes our techniques proposed above to answer Problem 2.
Starting from lines 1 to 7, we make use of the Jordan decomposition of the
matrix representation $\mathcal{M}_{\mathcal{E}}$ of $\mathcal{E}$ to
determine the period $p(\mathcal{G})$ and the stabilizer $\mathcal{E}_{\phi}$.
These computations allow us to obtain the periodically stable states
$\\{\eta_{k}\\}_{k=0}^{p(\mathcal{G})-1}$ of $\mathcal{G}$ and their
corresponding symbolic $\varepsilon$-neighborhood
$\\{\mathcal{N}_{\varepsilon}{(\eta_{k})}\\}_{k=0}^{p(\mathcal{G})-1}$ based
on the given approximation level $\varepsilon$. The steps involved in these
computations utilize Proposition 1 and Lemma 2. Afterwards, in line 8, we
determine the truncation number $K^{\varepsilon}$ using Lemma 3. Subsequently,
we compute $\\{L(\rho_{k})\\}_{k=0}^{K^{\varepsilon}-1}$, which represents the
symbols in $AP$ of the first $K^{\varepsilon}$ quantum states in the
trajectory $\sigma(\mathcal{G})$, from lines 9 to 11. Finally, in lines 12 and
13, we obtain an $\omega$-regular language
$\mathcal{N}_{\varepsilon}(\sigma(\mathcal{G}))$ that represents the symbolic
neighborhoods of the evolution $\sigma(\mathcal{G})$. The Büchi automaton
$A_{\varphi}$ for the MLTL formula $\varphi$ is constructed at line 14 by
means of a standard construction for an LTL formula $\varphi$ (see, e.g.,
[30]) while the Büchi automaton $A_{\mathcal{G}}$ at line 15 is obtained by an
ordinary lasso-shaped construction: it is enough to insert a new state between
each letter, make the state joining the stem and the lasso part accepting, and
use the accepting state as the target of the last action in the lasso. The two
operations on Büchi automata at lines 16 and 18 are standard: intersection and
emptiness reduce to automata product and strongly connected components
decomposition, respectively, which require quadratic time (cf. [30]). Language
inclusion, however, in general, requires exponential time and is PSPACE-
complete (cf. [30]); in our case, however, we can remain in quadratic time by
replacing the check
$\mathcal{L}(A_{\mathcal{G}})\subseteq\mathcal{L}(A_{\varphi})$ with
$\mathcal{L}(A_{\mathcal{G}})\cap\mathcal{L}(A_{\neg\varphi})=\emptyset$,
since constructing the Büchi automata $A_{\varphi}$ and $A_{\neg\varphi}$
requires the same asymptotic effort (cf. [30, Section 4.6.1]).

###### Remark 1

The complexity of approximately verifying MCs against interval LTL formulas in
the work of Agrawal et al. [17] is challenging to analyze and remains unknown.
This is because the BSCC decomposition analysis, which is relied upon, is not
an analytical method. Our model-checking algorithm, however, overcomes this by
utilizing the Jordan normal form to create a linear-algebraic representation
of the graph-theoretic (BSCC-based) model-checking algorithm mentioned in
[17]. Consequently, our model-checking algorithm (Algorithm 1) can effectively
verify MC models against interval LTL formulas. This capability stems from the
ability of QMCs to emulate MCs, as illustrated in Example 1, and the greater
expressiveness of our MLTL compared to interval LTL in [17], as discussed in
Section 4. Notably, MCs are inherently periodically stable, which extends to
the modeled QMCs, making our model-checking algorithm suitable for this
context. Additionally, while Agrawal et al. [17] did not offer a complexity
analysis for their algorithm, our method establishes the first upper bound on
the computational complexity of approximate model-checking for MCs against
interval LTL specifications from their work. Specifically, when using our
algorithm for model checking MCs, the complexity is reduced to
$\mathcal{O}(2^{\mathcal{O}(|\varphi|)}\cdot(K^{\varepsilon}+p(\mathcal{G}))+d^{4})$,
where $d$ represents the number of states in the MC. This reduction is due to
the fact that the complexity of computing the Jordan decomposition of the
$d$-by-$d$ stochastic matrix $P$ in MCs is $\mathcal{O}(d^{4})$. As a result,
the time complexity of calculating $K^{\varepsilon}$ and $p(\mathcal{G})$ is
also reduced to $\mathcal{O}(d^{4})$.

##  6 Case Studies

To demonstrate the utility of the model-checking techniques proposed in this
paper, we conducted case studies on quantum walks to investigate their
temporal linear-time properties. We completed a prototype for implementing our
model-checking algorithm and used it to automatically model check all MLTL
formulas provided in Example 3. The prototype was built using Python for the
quantum part to generate an $\omega$-regular language and Java for the
classical part to model check the language against LTL formulas by calling
Spot, a platform for LTL and $\omega$-automata manipulation [31].

Before conducting the verification process, it is crucial to ensure the
periodic stability of the QMC model for the quantum walk in Example 2. By
Proposition 1, this can be achieved by computing the eigenvalues of the model
and confirming that they only have 1 as the eigenvalue with a magnitude of
one. Armed with this information, we can then employ Algorithm 1 to verify the
properties outlined in Example 3. The experimental results for these
verifications can be found in Table 1.

The first experiment in Table 1 confirms the advantages of quantum walks over
classical random walks, which was previously established by Ambainis et al. in
[18]. The remaining two experiments aim to uncover new properties of quantum
walks. Moreover, we also utilized Algorithm 1 to verify these same properties
for one-dimensional unbiased classical random walks with absorbing boundaries,
which yielded contrasting results (false for the first experiment and true for
the last two experiments in Table 1). This confirms that these properties are
unique phenomena specific to quantum walks.

Table 1: The experimental result for position number $d=20$ and different initial states $\rho_{0}=|\psi_{0}\rangle\langle\psi_{0}|$. $|\phi_{0}\rangle$ | Formula $\varphi$ | Parameter $\varepsilon$
---|---|---
0.5 | 0.25 | 0.125
$|s_{1}\rangle|R\rangle$ | $\lozenge\square\langle M_{s_{0}},[1/\sqrt{2}-0.1,1/\sqrt{2}+0.1]\rangle$ | unknown | unknown | true
$|s_{10}\rangle|R\rangle$ | $\square\langle M_{s_{20}},[0,0.5)\rangle$ | unknown | unknown | false
$\square(\langle M_{s_{19}},(0.4,1]\rangle\implies\langle M_{s_{1}},(0.4,1]\rangle)$ | unknown | unknown | false

##  7 Conclusion

In this paper, we proposed a new quantum logic called measurement-based
linear-time temporal logic (MLTL) to specify the quantitative properties of
quantum Markov chains (QMCs). For model checking MLTL formulas, an algorithm
was developed. The measurement-based atomic propositions of MLTL build upon
the subspace-based quantum atomic propositions introduced by Birkhoff and von
Neumann [12]. Furthermore, we demonstrated the practical applicability of our
model-checking algorithm in quantum walks. This not only confirms the
previously established advantages discovered by Ambainis et al. [18] of
quantum walks over classical random walks, but also uncovers new phenomena
that are unique to quantum walks.

As future work, we note that the quantum walk in Example 2 can also be written
as a while-loop quantum program [29], and the absorbing probabilities are
exactly the termination probabilities of the program. Indeed, any quantum
program written in the While language can be modeled by a QMC [6]. So our
model-checking approach can be naturally applied in the verification of
program properties specified as MLTL formulas. Therefore, we plan to apply our
model-checking algorithms to verify quantum programs. Moreover, it would be
intriguing to broaden the application of the methods presented in this paper
to verify the behavior of non-periodically stable QMCs. One possible approach
is that any non-periodically stable QMC will be close to a periodically stable
one with arbitrary precision, as any irrational number (eigenvalue) will be
close to a rational number (eigenvalue) with the same precision.

## References

  * [1] Christel Baier and Joost-Pieter Katoen.  Principles of model checking.  MIT press, 2008.
  * [2] Mingsheng Ying and Yuan Feng.  Model-checking quantum systems.  National Science Review, 6(1):28–31, 2019.
  * [3] Mingsheng Ying and Yuan Feng.  Model Checking Quantum Systems: Principles and Algorithms.  Cambridge University Press, 2021.
  * [4] Francesco Ticozzi and Lorenza Viola.  Quantum Markovian subsystems: Invariance, attractivity, and control.  IEEE Transactions on Automatic Control, 53(9):2048–2063, 2008.
  * [5] Ji Guan, Yuan Feng, and Mingsheng Ying.  The structure of decoherence-free subsystems.  arXiv preprint arXiv:1802.04904, 2018.
  * [6] Mingsheng Ying.  Foundations of Quantum Programming.  Morgan Kaufmann, 2016.
  * [7] Michael M Wolf.  Quantum channels & operations: Guided tour.  Lecture notes available at https://mediatum.ub.tum.de/doc/1701036/document.pdf, 2012.
  * [8] Andris Ambainis.  Quantum walks and their algorithmic applications.  International Journal of Quantum Information, 1:507–518, 2003.
  * [9] Julia Kempe.  Quantum random walks: an introductory overview.  Contemporary Physics, 44(4):307–327, 2003.
  * [10] Stephane Attal, Francesco Petruccione, Christophe Sabot, and Ilya Sinayskiy.  Open quantum random walks.  Journal of Statistical Physics, 147(4):832–852, 2012.
  * [11] Yuan Feng, Nengkun Yu, and Mingsheng Ying.  Model checking quantum Markov chains.  Journal of Computer and System Sciences, 79(7):1181–1198, 2013.
  * [12] Garrett Birkhoff and John von Neumann.  The logic of quantum mechanics.  Annals of mathematics, pages 823–843, 1936.
  * [13] Cristopher Moore and James P Crutchfield.  Quantum automata and quantum grammars.  Theoretical Computer Science, 237(1-2):275–306, 2000.
  * [14] Mingsheng Ying, Yangjia Li, Nengkun Yu, and Yuan Feng.  Model-checking linear-time properties of quantum systems.  ACM Transactions on Computational Logic (TOCL), 15(3):22, 2014.
  * [15] Yangjia Li and Mingsheng Ying.  (Un)decidable problems about reachability of quantum systems.  In CONCUR 2014–Concurrency Theory: 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings 25, pages 482–496. Springer, 2014.
  * [16] Amir Pnueli.  The temporal logic of programs.  In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pages 46–57. IEEE Computer Society, 1977.
  * [17] Manindra Agrawal, Sundararaman Akshay, Blaise Genest, and PS Thiagarajan.  Approximate verification of the symbolic dynamics of Markov chains.  Journal of the ACM (JACM), 62(1):2, 2015.
  * [18] Andris Ambainis, Eric Bach, Ashwin Nayak, Ashvin Vishwanath, and John Watrous.  One-dimensional quantum walks.  In Proceedings of the thirty-third annual ACM symposium on Theory of computing (STOC), pages 37–49. ACM, 2001.
  * [19] Shenggang Ying, Yuan Feng, Nengkun Yu, and Mingsheng Ying.  Reachability probabilities of quantum Markov chains.  In International Conference on Concurrency Theory, pages 334–348. Springer, 2013.
  * [20] Salvador Elías Venegas-Andraca.  Quantum walks: a comprehensive review.  Quantum Information Processing, 11(5):1015–1106, 2012.
  * [21] Michael A. Nielsen and Isaac L. Chuang.  Quantum computation and quantum information.  Cambridge university press, 2010.
  * [22] Man-Duen Choi.  Completely positive linear maps on complex matrices.  Linear algebra and its applications, 10(3):285–290, 1975.
  * [23] Ji Guan and Nengkun Yu.  A probabilistic logic for verifying continuous-time Markov chains.  In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 3–21. Springer, 2022.
  * [24] Moshe Y Vardi.  Probabilistic linear-time model checking: An overview of the automata-theoretic approach.  In International AMAST Workshop on Aspects of Real-Time Systems and Concurrent and Distributed Software, pages 265–276. Springer, 1999.
  * [25] Bernhard Baumgartner and Heide Narnhofer.  The structures of state space concerning quantum dynamical semigroups.  Reviews in Mathematical Physics, 24(02):1250001, 2012.
  * [26] Ji Guan, Yuan Feng, and Mingsheng Ying.  Decomposition of quantum Markov chains and its applications.  Journal of Computer and System Sciences, 2018.
  * [27] Robert G Gallager.  Discrete stochastic processes, volume 321.  Springer Science & Business Media, 2012.
  * [28] Godfrey Harold Hardy and Edward Maitland Wright.  An introduction to the theory of numbers.  Oxford university press, 1979.
  * [29] Mingsheng Ying, Nengkun Yu, Yuan Feng, and Runyao Duan.  Verification of quantum programs.  Science of Computer Programming, 78:1679–1700, 2013.
  * [30] Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors.  Handbook of Model Checking.  Springer, 2018.
  * [31] Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard, and Henrich Lauko.  From Spot 2.0 to Spot 2.10: What’s new?  In Proceedings of the 34th International Conference on Computer Aided Verification (CAV’22), volume 13372 of Lecture Notes in Computer Science, pages 174–187. Springer, August 2022.
  * [32] Ji Guan, Yuan Feng, and Mingsheng Ying.  Super-activating quantum memory with entanglement.  Quantum Inf. Comp., 18:1115–1124, 2018.
  * [33] Victor V. Albert.  Asymptotics of quantum channels: conserved quantities, an adiabatic limit, and matrix product states.  Quantum, 3:151, June 2019.
  * [34] Daniel Burgarth, Giulio Chiribella, Vittorio Giovannetti, Paolo Perinotti, and Kazuya Yuasa.  Ergodic and mixing quantum channels in finite dimensions.  New Journal of Physics, 15, 2013.
  * [35] Roger A. Horn and Charles R. Johnson.  Matrix analysis.  Cambridge university press, 2013.

## Appendix

##  Appendix 0.A Visualization of the Evolution of Quantum Walks

Figure 1: The dynamics of one-dimensional quantum walk with boundaries in one
step

To gain a better understanding of the evolution of quantum walks, it is
necessary to introduce the concept of _amplitude distribution_ from quantum
physics. As stated in Section 2, in a Hilbert space
$\mathcal{H}=\operatorname{span}\\{|s_{0}\rangle,\dotsc,|s_{d}\rangle\\}$, any
quantum pure state $|\psi\rangle$ can be expressed as
$|\psi\rangle=\sum_{k=0}^{d}a_{k}|s_{k}\rangle$, where $a_{k}$ is a complex
number and referred to as the _amplitude_ of $|\psi\rangle$. The amplitude
distribution $(a_{0},\dotsc,a_{d})$ is a unit complex vector
($a_{0}a_{0}^{*}+\ldots+a_{d}a_{d}^{*}=1$) formed by the set of amplitudes
$\\{a_{0},\dotsc,a_{d}\\}$. It is important to note that the amplitude
distribution can also be used to represent a probability distribution
($a_{0}a_{0}^{*},\dotsc,a_{d}a_{d}^{*}$). Conversely, a probability
distribution $(p_{0},\dotsc,p_{d})$ can be expressed as an amplitude
distribution $(\sqrt{p_{0}},\dotsc,\sqrt{p_{d}})$.

To further illustrate the dynamic nature of the quantum walk, we can examine
the evolution of the state at each step of the walk. This can be visualized in
Fig. 1, where the state at position $s_{k}$ is shown. The cases at other
positions follow a similar pattern. Initially, the current state of the
quantum system is represented as $|s_{k}\rangle|R\rangle$ (on the left side of
Fig. 1) or $|s_{k}\rangle|L\rangle$ (on the right side of Fig. 1), indicating
the state at position $s_{k}$ with the direction either right or left,
respectively.

To begin the walk, we perform a measurement $\\{M_{yes},M_{no}\\}$ on the
current state to determine if the position $s_{k}$ corresponds to the
absorbing positions $s_{0}$ or $s_{d}$. If it is an absorbing position, the
walk terminates. If not, the walk proceeds to the next two sub-steps, which
involve moving the current position.

Next, a coin (Hadamard operator) $U_{H}$ is tossed to decide the direction of
movement. This generates two possibilities with different directions and
amplitude distributions, determined by the current state. Specifically, if the
current state is $|s_{k}\rangle|R\rangle$ (on the left side of Fig. 1), the
amplitude distribution is $(\frac{1}{\sqrt{2}},\frac{1}{\sqrt{2}})$,
representing the quantum walk moving to the right and left with a probability
distribution of $(\frac{1}{2},\frac{1}{2})$. Similarly, for the state
$|s_{k}\rangle|L\rangle$ (on the right side of Fig. 1), the amplitude
distribution is $(\frac{1}{\sqrt{2}},-\frac{1}{\sqrt{2}})$, indicating the
quantum walk moving to the right and left with a probability distribution of
$(\frac{1}{2},\frac{1}{2})$.

After determining the direction, the walk moves one position to the right or
left based on the amplitude distribution by performing a shift operator
$U_{S}$. This completes one step of the walk, and the process continues with
the updated current state.

It is important to note that the elements of the amplitude distribution can be
negative, such as $-\frac{1}{\sqrt{2}}$. As a result, when computing the total
amplitude of the walk, subtractions occur, leading to some amplitudes
decreasing in absolute value (probability) while others increase. This
phenomenon, known as _quantum interference_ , results in the quantum walk
exhibiting behavior that is significantly different from classical random
walks. For example, the unbiased walk in Example 2 starting at the central
position will exhibit a non-symmetric evolution. Our model-checking algorithm
has identified and verified several properties related to this behavior.

##  Appendix 0.B Proof of Proposition 1

In this section, we give an easily checkable characterization of the periodic
stability of QMCs to complete the proof of Proposition 1.

Before proceeding, let us establish some mathematical notations from linear
algebra that will be used later.

Firstly, it should be noted that any linear map $T$ on $\mathcal{L(H)}$ can
have a maximum of $d^{2}$ (where $d=\dim(\mathcal{H})$) complex eigenvalues
$\lambda$ that satisfy $T(A)=\lambda A$ for some non-zero operator
$A\in\mathcal{L(H)}$. We denote the _spectrum_ of $T$ as $\mathit{spec}(T)$,
which represents the set of all eigenvalues of $T$. The spectral radius of $T$
is defined as $\varrho(T)=\max\\{\,|\lambda|:\lambda\in\mathit{spec}(T)\,\\}$.
In particular, for any super-operator $\mathcal{E}$ on $\mathcal{H}$, it holds
that $\varrho(\mathcal{E})=1$ [7, Proposition 6.1]. We denote the set of
eigenvalues of $T$ with a magnitude of one as
$\kappa(T)=\\{\,\lambda\in\mathit{spec}(T):|\lambda|=1\,\\}.$ It is important
to note that the calculation of $\mathit{spec}(\mathcal{E})$ can be simplified
to the calculation of $\mathit{spec}(\mathcal{M}_{\mathcal{E}})$, as shown in
Lemma 1. Furthermore, the _support_ of a quantum state $\rho$, denoted as
$\mathit{supp}(\rho)$, is a subspace of $\mathcal{H}$ spanned by the
eigenvectors corresponding to the non-zero eigenvalues of $\rho$. If
$\mathit{supp}(\rho)=\mathcal{H}$, then $\rho$ is referred to as a _full-rank_
state. $\rho$ is considered a _stationary state_ of $\mathcal{E}$ if and only
if $\mathcal{E}(\rho)=\rho$. Additionally, a stationary state $\rho$ is
classified as _maximal_ if for any other stationary state $\sigma$ of
$\mathcal{E}$, the support of $\sigma$ is a subspace of the support of $\rho$,
i.e., $\mathit{supp}(\sigma)\subseteq\mathit{supp}(\rho)$. It is important to
note that, for a given super-operator $\mathcal{E}$, the support of any
maximal stationary state of $\mathcal{E}$ remains the same [26].

Let $(\mathcal{H},\mathcal{E},\rho_{0})$ be a QMC where
$\mathcal{M}_{\mathcal{E}}$ represents the matrix $\mathcal{E}$ and
$\mathcal{M}_{\mathcal{E}}=SJS^{-1}$ is its Jordan decomposition. For each
$0\leq k\leq d^{2}-1$ where $d=\dim(\mathcal{H})$, let $|s_{k}\rangle$ be the
$k$-th column vector of $S$. Since $S$ is invertible, the vectors
$|s_{k}\rangle$ form a basis of the Hilbert space
$\mathcal{H}\otimes\mathcal{H}$. Therefore, for any quantum state
$\rho\in\mathcal{D(H)}$, its vectorization
$|\rho\rangle\in\mathcal{H}\otimes\mathcal{H}$ can be uniquely represented as
a linear combination of these vectors:
$|\rho\rangle=\sum_{k}a_{k}|s_{k}\rangle$. Let

$\kappa(\rho)=\\{\,\lambda\in\kappa(\mathcal{E}):\text{$\mathcal{M}_{\mathcal{E}}|s_{k}\rangle=\lambda|s_{k}\rangle$
for some $k$ with $a_{k}\neq 0$}\,\\}$

be the set of eigenvalues of $\mathcal{M}_{\mathcal{E}}$ with a magnitude of
one that contribute non-trivially to $|\rho\rangle$.

We can now state the following proposition, which provides a method to
determine whether a QMC $\mathcal{G}$ is periodically stable, as mentioned in
Proposition 1.

###### Proposition 2

A QMC $(\mathcal{H},\mathcal{E},\rho_{0})$ is periodically stable if and only
if $\kappa(\rho_{0})$ does not contain any element of the form
$e^{i2\pi\psi}$, where $\psi$ is an irrational number. Furthermore, the
complexity of checking periodic stability is $\mathcal{O}(d^{8})$, where
$d=\dim(\mathcal{H})$.

###### Proof

First, note that for any $m>0$ and $\rho\in\mathcal{D(H)}$,
$|\mathcal{E}^{m}(\rho)\rangle=M^{m}_{\mathcal{E}}|\rho\rangle$. Thus
$(\mathcal{H},\mathcal{E},\rho_{0})$ is periodically stable if and only if
there exists an integer $\theta>0$ such that
$\lim_{n\to\infty}\mathcal{M}_{\mathcal{E}}^{n\theta}|\rho_{0}\rangle$ exists.
Let $|\rho_{0}\rangle=\sum_{j}a_{j}|s_{j}\rangle$. For any $0\leq j\leq
d^{2}-1$, if $|s_{j}\rangle$ is an (generalized) eigenvector of
$\mathcal{M}_{\mathcal{E}}$ corresponding to an eigenvalue with magnitude
strictly smaller than $1$, then
$\lim_{n\to\infty}\mathcal{M}_{\mathcal{E}}^{n\theta}|s_{j}\rangle=0$ for any
$\theta$. Thus we only need to care about $|s_{j}\rangle$ corresponding to
eigenvalues with a magnitude of one. Following [32, Lemma 2],
$\mathcal{P}\circ\mathcal{E}$ shares with $\mathcal{E}$ the same eigenvalues
with a magnitude of one and the corresponding eigenvectors, where
$\mathcal{P}(\rho)=P\rho P$ for all $\rho$, and $P$ is the projector onto the
support of the maximal stationary state. Therefore, w.l.o.g., we assume that
$\mathcal{E}$ has a full-rank stationary state. This kind of $\mathcal{E}$ is
called _faithful_ in [33].

Furthermore, for faithful $\mathcal{E}$, the Kraus operators $\\{E_{i}\\}$
admit a diagonal form with respect to an appropriate decomposition
$\mathcal{H}=\oplus_{k=0}^{t-1}\mathcal{H}_{k}$ [19, 34], where $\oplus$
denotes the _direct sum_ operation. To be specific, for all $i$,

$E_{i}=\oplus_{k=0}^{t-1}E_{i,k}=\left[\begin{array}[]{cccc}E_{i,0}&&&\\\
&E_{i,1}&&\\\ &&\ddots&\\\ &&&E_{i,t-1}\end{array}\right]$

where $E_{i,k}\in\mathcal{L}(\mathcal{H}_{k})$, so $\mathcal{M}_{\mathcal{E}}$
has the corresponding structure

$\mathcal{M}_{\mathcal{E}}=\bigoplus_{k,l}\mathcal{M}_{k,l}$

where $\mathcal{M}_{k,l}=\sum_{i}E_{i,k}\otimes E_{i,l}^{*}$. Furthermore, for
any $\theta>0$ we have

$\lim_{n\to\infty}\mathcal{M}_{\mathcal{E}}^{n\theta}|\rho_{0}\rangle=\bigoplus_{k,l}\lim_{n\to\infty}\mathcal{M}_{k,l}^{n\theta}|\rho_{0,k,l}\rangle,$
(6)

where $|\rho_{0,k,l}\rangle$ is the restriction of $|\rho_{0}\rangle$ onto
$\mathcal{H}_{k}\otimes\mathcal{H}_{l}$, i.e.,
$|\rho_{0}\rangle=\oplus_{k,l}|\rho_{0,k,l}\rangle$. Now it is easy to see
that $\lim_{n\to\infty}\mathcal{M}_{\mathcal{E}}^{n\theta}|\rho_{0}\rangle$
exists if and only if for any $k$ and $l$,
$\lim_{n\to\infty}\mathcal{M}_{k,l}^{n\theta}|\rho_{0,k,l}\rangle$ exists.

To verify the existence of
$\lim_{n\to\infty}\mathcal{M}_{k,l}^{n\theta}|\rho_{0,k,l}\rangle$, let

$|\rho_{0}\rangle=\sum_{j}a_{j}|s_{j}\rangle=\bigoplus_{k,l}\sum_{j}a_{j}|s_{j,k,l}\rangle,$

where $|s_{j,k,l}\rangle$ is the restriction of $|s_{k}\rangle$ onto
$\mathcal{H}_{k}\otimes\mathcal{H}_{l}$. Then
$|\rho_{0,k,l}\rangle=\sum_{j}a_{j}|s_{j,k,l}\rangle$. Define

$\kappa(\rho_{0,k,l})=\\{\,\lambda\in\kappa(\mathcal{M}_{k,l}):\text{$\mathcal{M}_{k,l}|s_{j,k,l}\rangle=\lambda|s_{j,k,l}\rangle$
for some $j$ with $a_{j}\neq 0$}\,\\}.$

For any $0\leq j\leq d^{2}-1$ and $0\leq k,l\leq m-1$, we have two cases to
consider:

  * •

if $|s_{j,k,l}\rangle$ is a (generalized) eigenvector of $\mathcal{M}_{k,l}$
corresponding to an eigenvalue with magnitude strictly smaller than $1$, then
$\lim_{n\to\infty}\mathcal{M}_{\mathcal{E}}^{n\theta_{j}}|s_{j,k,l}\rangle=0$
for any $\theta_{j}$;

  * •

if $|s_{j,k,l}\rangle$ is an eigenvector of $\mathcal{M}_{k,l}$ corresponding
to an eigenvalue with a magnitude of one, then
$\mathcal{M}_{k,l}^{n}|s_{j,k,l}\rangle=e^{i2\pi\psi_{j,k,l}n}|s_{j,k,l}\rangle$
for some $\psi_{j,k,l}$. Thus we have
$\lim_{n\to\infty}\mathcal{M}_{\mathcal{E}}^{n\theta_{j}}|s_{j,k,l}\rangle$
exists for some $\theta_{j}>0$ if and only if $\psi_{j,k,l}$ is rational and
$\theta_{j}\psi_{j,k,l}$ is an integer [28].

Note that the matrices $\mathcal{M}_{k,l}$’s have the following spectral
properties (cf. [5]): for any $k$ and $l$,
$\kappa(\mathcal{M}_{k,l})=\emptyset$ or
$\kappa(\mathcal{M}_{k,l})=\\{\exp(i2\pi(r+\psi_{k,l})/N_{k,l})\\}_{r=0}^{N_{k,l}-1}$,
where $N_{k,l}$ is a positive integer and $\psi$ is a real number. Thus
$\lim_{n\to\infty}\mathcal{M}_{k,l}^{n\theta}|\rho_{0,k,l}\rangle$ exists if
and only if $\kappa(\rho_{0,k,l})$ does not contain any element of the form
$e^{i2\pi\psi}$ for some irrational number $\psi$. We complete the proof by
noting that $\kappa(\rho)=\\{\,\lambda\in\kappa(\rho_{0,k,l}):0\leq k,l\leq
m-1\,\\}$. ∎

It is important to highlight that the proof of Proposition 2 offers a method
to check the periodic stability of QMCs. The main computational cost lies in
the Jordan decomposition $\mathcal{M}_{\mathcal{E}}=SJS^{-1}$ of
$\mathcal{M}_{\mathcal{E}}$. It is widely recognized that the complexity of
the Jordan decomposition for an $n$-by-$n$ matrix is $\mathcal{O}(n^{4})$.
Therefore, for a $d^{2}$-by-$d^{2}$ matrix $\mathcal{M}_{\mathcal{E}}$, the
cost is $\mathcal{O}(d^{8})$. Consequently, the aforementioned proof of
Proposition 2 concludes the proof of the first part of Proposition 1.

###### Corollary 1

Let $\mathcal{G}=(\mathcal{H},\mathcal{E},\rho_{0})$ be a periodically stable
QMC with $d=\dim(\mathcal{H})$.

  * •

If we express $\kappa(\rho_{0})$ as

$\kappa(\rho_{0})=\\{\,e^{2\pi ip_{k}/q_{k}}:\text{$p_{k}$ and $q_{k}$ are
coprime positive integers}\,\\}_{k},$

then $p(\mathcal{G})=\operatorname{lcm}\\{q_{k}\\}_{k}$, the least common
multiple of $\\{q_{k}\\}_{k}$.

  * •

For any positive integer $\theta$,
$\lim_{n\to\infty}\mathcal{E}^{n\theta}(\rho_{0})$ exists if and only if
$p(\mathcal{G})$ divides $\theta$.

Corollary 1 presents a technique for calculating $p(\mathcal{G})$ by
determining the Jordan decomposition of a $d^{2}$-by-$d^{2}$ matrix
$\mathcal{M}_{\mathcal{E}}$ and then evaluating $\kappa(\rho_{0})$ using its
definition. The time complexity of this method is $\mathcal{O}(d^{8})$. This
concludes the proof of the second part of Proposition 1.

##  Appendix 0.C Proof of Lemma 1

######  Proof (of Lemma 1)

To begin, let us establish the transformation of $\mathcal{E}$ on
$\mathcal{H}_{1}$ and its corresponding matrix representation on
$\mathcal{H}_{1}\otimes\mathcal{H}_{2}$ as shown below:

$\mathcal{E}(A)={\rm tr}_{2}(\mathcal{M}_{\mathcal{E}}(A\otimes
I)|\Omega\rangle\langle\Omega|)$, for any $A\in\mathcal{L}(\mathcal{H}_{1})$.
(7)

Here, ${\rm tr}_{2}$ denotes the _partial trace_ operation on the second
Hilbert space [21]. Mathematically, ${\rm tr}_{2}(\,\mathord{\cdot}\,)$ is a
linear map from $\mathcal{L}(\mathcal{H}_{1}\otimes\mathcal{H}_{2})$ to
$\mathcal{L}(\mathcal{H}_{1})$. Given that
$\mathcal{H}=\operatorname{span}\\{|s_{0}\rangle,\dotsc,|s_{d-1}\rangle\\}$,
we can express ${\rm tr}_{2}(\,\mathord{\cdot}\,)$ as follows:

${\rm tr}_{2}(\mathcal{M})=\sum_{k}(I\otimes\langle
s_{k}|)\mathcal{M}(I\otimes|s_{k}\rangle)$, for all
$\mathcal{M}\in\mathcal{L}(\mathcal{H}_{1}\otimes\mathcal{H}_{2})$.

Here, $I$ represents the identity operator on $\mathcal{H}_{1}$. By utilizing
the transformation in Eq. (7), we can readily prove that
$\mathcal{E}(A)=\lambda A$ if and only if
$\mathcal{M}_{\mathcal{E}}|A\rangle=\lambda|A\rangle$, where
$A\in\mathcal{L(H)}$ is not a zero matrix. ∎

##  Appendix 0.D Proof of Lemma 2

######  Proof (of Lemma 2)

Let $\theta=p(\mathcal{G})$. Based on the proof of Proposition 2, Corollary 1,
and the construction of the stabilizer $\mathcal{E}_{\phi}$, we can conclude
that

$\text{$\lim_{n\to\infty}\mathcal{E}^{n\theta+k}(\rho_{0})=\mathcal{E}_{\phi}(\mathcal{E}^{k}(\rho_{0}))$
for any integer $0\leq k\leq\theta-1$}.$

In other words, the set
$\\{\mathcal{E}_{\phi}(\mathcal{E}^{k}(\rho_{0}))\\}_{0\leq k<p(\mathcal{G})}$
consists of the periodically stable states of $\mathcal{G}$. The process of
obtaining this set has the same computational complexity as that of
constructing $\mathcal{E}_{\phi}$, which is $\mathcal{O}(d^{8})$ for the
Jordan decomposition of the $d^{2}$-by-$d^{2}$ matrix
$\mathcal{M}_{\mathcal{E}}$, as discussed in Subsection 5.1. ∎

##  Appendix 0.E Proof of Lemma 3

To prove Lemma 3, we need to characterize the $\varepsilon$-neighborhoods of
the quantum state $\rho\in\mathcal{D(H)}\subseteq\mathcal{L(H)}$ and the
super-operator $\mathcal{E}\in\mathcal{L(\mathcal{L(H)})}$. Here,
$\mathcal{L(\mathcal{L(H)})}$ represents the set of all linear operators from
$\mathcal{L(H)}$ to $\mathcal{L(H)}$. To do this, we must introduce norms on
$\mathcal{L(H)}$ and $\mathcal{L(\mathcal{L(H)})}$. The Schatten 2-norm (also
known as the Hilbert-Schmidt norm) on $\mathcal{L(H)}$ has already been
introduced in Definition 4 to define the $\varepsilon$-neighborhood of $\rho$.
Now, we introduce an additional norm on $\mathcal{L(\mathcal{L(H)})}$, and we
choose to utilize the Schatten 2-norm on $\mathcal{L(H)}$ to induce an
operator norm on $\mathcal{L(\mathcal{L(H)})}$. It is important to note that
the results presented here are applicable to any other norm because all norms
in a finite-dimensional Hilbert space are equivalent [35].

###### Definition 6

Given a Hilbert space $\mathcal{H}$, the operator norm
$\|\,\mathord{\cdot}\,\|_{o}$ on $\mathcal{L(\mathcal{L(H)})}$ induced by the
Schatten 2-norm $\|\,\mathord{\cdot}\,\|$ is defined as follows:

$\|T\|_{o}:=\sup\\{\,\|T(A)\|:\text{$A\in\mathcal{L(H)}$ with $\|A\|=1$}\,\\}$
for any $T\in\mathcal{L(\mathcal{L(H)})}$.

Furthermore, for simplicity, we will refer to $\|\,\mathord{\cdot}\,\|_{o}$ as
$\|\,\mathord{\cdot}\,\|$ unless there is potential confusion.

Based on the given norm and the fact that $\|A\|=\sqrt{{\rm
tr}(A^{\dagger}A)}=\sqrt{\langle A|A\rangle}$, it can be easily shown that for
any super-operator $\mathcal{E}$,

$\|\mathcal{E}\|=\|\mathcal{M}_{\mathcal{E}}\|=\max_{\lambda\in\mathit{spec}(\mathcal{M}_{\mathcal{E}}^{{\dagger}}\mathcal{M}_{\mathcal{E}})}\sqrt{\lambda}.$

In other words, $\|\mathcal{E}\|$ represents the maximum singular value of
$\mathcal{M}_{\mathcal{E}}$, which is equal to 1 for the super-operator
$\mathcal{E}$ (i.e., $\|\mathcal{E}\|=1$). With this, for any super-operators
$\mathcal{E}_{1}$, $\mathcal{E}_{2}$, and $\mathcal{F}$, we have

$\|(\mathcal{E}_{1}-\mathcal{E}_{2})\circ\mathcal{F}\|\leq\|\mathcal{E}_{1}-\mathcal{E}_{2}\|\cdot\|\mathcal{F}\|=\|\mathcal{E}_{1}-\mathcal{E}_{2}\|.$
(8)

The inequality is a result of the sub-multiplicative property of the operator
norm, which states that $\|T_{1}T_{2}\|\leq\|T_{1}\|\cdot\|T_{2}\|$.

Furthermore, for any $\rho\in\mathcal{D(H)}$ and super-operators
$\mathcal{E}_{1}$ and $\mathcal{E}_{2}$, we have

$\|\mathcal{E}_{1}(\rho)-\mathcal{E}_{2}(\rho)\|\leq\|\mathcal{E}_{1}-\mathcal{E}_{2}\|\cdot\|\rho\|\leq\|\mathcal{E}_{1}-\mathcal{E}_{2}\|.$
(9)

The second inequality follows from the fact that $\|\rho\|\leq 1$.

To prove Lemma 3, an essential result of the asymptotic property of
$\mathcal{E}$ characterized by $\mathcal{E}_{\phi}$ from [7] is also needed.
This result is based on the _Jordan condition number_.

It is important to note that the Jordan decomposition
$\mathcal{M}_{\mathcal{E}}=SJS^{-1}$ is not unique, and we define

$\alpha(\mathcal{E})=\inf_{S}\\{\,\|S\|\cdot\|S^{-1}\|:\text{$S^{-1}\mathcal{M}_{\mathcal{E}}S$
is in Jordan normal form}\,\\}$

as the _Jordan condition number_ [7] of $\mathcal{E}$.

######  Lemma 4 (cf. [7, Theorem 8.23])

For any $n>0$ we have

$C^{-1}\omega^{n}n^{d_{\omega}-1}\leq\|\mathcal{M}_{\mathcal{E}}^{n}-\mathcal{M}_{\mathcal{E}_{\psi}}^{n}\|\leq
C\omega^{n}n^{d_{\omega}-1}$

where $\mathcal{E}_{\psi}=\mathcal{E}\circ\mathcal{E}_{\phi}$,
$\omega=\sup\\{\,|\lambda|:\lambda\in\mathit{spec}(\mathcal{E}),|\lambda|<1\,\\}$
is the largest modulus of eigenvalues of $\mathcal{E}$ in the interior of the
unit disc, $d_{\omega}$ is the dimension of the largest Jordan block
corresponding to eigenvectors of modulus $\omega$, and

$C=\begin{cases}\alpha(\mathcal{E})&\text{if $d_{\omega}=1$,}\\\
\alpha(\mathcal{E})(\omega(d_{\omega}-1))^{d_{\omega}-1}&\text{if
$1<d_{\omega}\leq n+1.$}\end{cases}$

Now, we present the proof of Lemma 3.

######  Proof (of Lemma 3)

Let $\theta=p(\mathcal{G})$. By Lemma 2,
$\\{\mathcal{E}_{\phi}(\mathcal{E}^{k}(\rho_{0}))\\}_{0\leq k<p(\mathcal{G})}$
are the periodically stable states of $\mathcal{G}$, i.e.,

$\lim_{n\to\infty}\mathcal{E}^{n}(\rho_{0})=\mathcal{E}_{\phi}(\mathcal{E}^{n\operatorname{mod}\theta}(\rho_{0})).$

Thus for any $\varepsilon>0$, there exists a positive integer
$K^{\varepsilon}$ such that for all $n>K^{\varepsilon}$,

$\|\mathcal{E}^{n}(\rho_{0})-\mathcal{E}_{\phi}(\mathcal{E}^{n\operatorname{mod}\theta}(\rho_{0}))\|<\varepsilon$

as desired.

To determine $K^{\varepsilon}$, we recall from Lemma 4 that

$C^{-1}\omega^{n}n^{d_{\omega}-1}\leq\|\mathcal{M}_{\mathcal{E}}^{n}-\mathcal{M}_{\mathcal{E}_{\psi}}^{n}\|\leq
C\omega^{n}n^{d_{\omega}-1}.$

Let $n=m\theta+k$ with $0\leq k\leq\theta-1$, and note that
$\mathcal{E}_{\psi}^{m\theta}(\rho_{0})=\mathcal{E}_{\phi}(\rho_{0})$ by
Corollary 1. We have

$\|\mathcal{E}^{m\theta+k}(\rho_{0})-\mathcal{E}_{\phi}(\mathcal{E}^{k}(\rho_{0}))\|=\|\mathcal{E}^{m\theta+k}(\rho_{0})-\mathcal{E}_{\psi}^{m\theta+k}(\rho_{0})\|\leq\|\mathcal{E}^{m\theta}-\mathcal{E}_{\psi}^{m\theta}\|$

where the inequality follows from Eqs. (8) and (9). So we can simply set
$K^{\varepsilon}$ to be the minimal integer satisfying

$\displaystyle\text{$C\omega^{K^{\varepsilon}}{(K^{\varepsilon})}^{d_{\omega}-1}<\varepsilon$
\quad and \quad$K^{\varepsilon}+1>d_{\omega}$},$ (10)

where the second inequality comes from the requirement of $C$ in Lemma 4.
Finally, the computation of $C$ boils down to the Jordan decomposition of
$\mathcal{E}$, which makes the time complexity of calculating
$K^{\varepsilon}$ to be $\mathcal{O}(d^{8})$. ∎

##  Appendix 0.F Proof of Theorem 5.1

######  Proof (of Theorem 5.1)

To see the correctness of Algorithm 1, we can proceed with a detailed
examination of its steps immediately following the presentation of Theorem
5.1.

To analyze the complexity of Algorithm 1, we first focus on the computation of
the $\omega$-regular language $\mathcal{N}_{\varepsilon}(\sigma(\mathcal{G}))$
from lines 1 to 13. The main computational tasks include determining the
period $\mathcal{P}(\mathcal{G})$, the stabilizer $\mathcal{E}_{\phi}$, the
periodically stable state $\\{\eta_{k}\\}_{k=0}^{p(\mathcal{G})-1}$, and the
truncation number $K^{\varepsilon}$. These values can be obtained using
Proposition 1 and Lemmas 2 and 3. The overall complexity is
$\mathcal{O}(d^{8})$, with the main cost being the Jordan decomposition of a
$d^{2}$-by-$d^{2}$ matrix $\mathcal{M}_{\mathcal{E}}$. It is well-known that
the complexity of the Jordan decomposition for an $n$-by-$n$ matrix is
$\mathcal{O}(n^{4})$. Therefore, for a $d^{2}$-by-$d^{2}$ matrix
$\mathcal{M}_{\mathcal{E}}$, the cost is $\mathcal{O}(d^{8})$.

Once we have obtained the $\omega$-regular language
$\mathcal{N}_{\varepsilon}(\sigma(\mathcal{G}))$, we can utilize the standard
Büchi automata approach from Line 14 to the end of Algorithm 1 to perform
model checking on $\mathcal{N}_{\varepsilon}(\sigma(\mathcal{G}))$ against a
LTL (MLTL) formula $\varphi$. This approach allows us to address the
verification problem outlined in Problem 2. As said in the analysis after the
statement of Theorem 5.1, the main source of complexity is the model checking
of $\mathcal{N}_{\varepsilon}(\sigma(\mathcal{G}))$ against the formulas
$\varphi$ and $\neg\varphi$: the former is used at line 16 while the latter at
line 18 since checking
$\mathcal{L}(A_{\mathcal{G}})\subseteq\mathcal{L}(A_{\varphi})$ is equivalent
to verifying
$\mathcal{L}(A_{\mathcal{G}})\cap\mathcal{L}(A_{\neg\varphi})=\emptyset$.
These operations are done by constructing the Büchi automata $A_{\varphi}$ and
$A_{\neg\varphi}$ for $\varphi$ and $\neg\varphi$, respectively, and checking
the emptiness of their language intersection with
$\mathcal{L}(A_{\mathcal{G}})$, i.e., with
$\mathcal{N}_{\varepsilon}(\sigma(\mathcal{G}))$. The complexity of model
checking an $\omega$-regular language with a length of
$K^{\varepsilon}+p(\mathcal{G})$ for a given LTL (MLTL) formula
$\varphi^{\prime}$ is
$\mathcal{O}(2^{\mathcal{O}(|\varphi^{\prime}|)}\cdot(K^{\varepsilon}+p(\mathcal{G})))$
[30, 1]. Thus the two checks at lines 16 and 18 have a total complexity of
$\mathcal{O}((2^{\mathcal{O}(|\varphi|)}+2^{\mathcal{O}(|\neg\varphi|)})\cdot(K^{\varepsilon}+p(\mathcal{G})))$.
Since it is widely accepted in the model checking community that the Büchi
automata $A_{\varphi}$ and $A_{\neg\varphi}$ can be obtained with the same
complexity $2^{\mathcal{O}(|\varphi|)}$ (cf. the automaton construction given
in [1, Theorem 5.37] or in [30, Section 4.6.1]), the term
$2^{\mathcal{O}(|\varphi|)}+2^{\mathcal{O}(|\neg\varphi|)}$ becomes $2\cdot
2^{\mathcal{O}(|\varphi|)}$. Therefore, the complexity for performing model
checking on the $\omega$-regular language
$\mathcal{N}_{\varepsilon}(\sigma(\mathcal{G}))$ is
$\mathcal{O}(2^{\mathcal{O}(|\varphi|)}\cdot(K^{\varepsilon}+p(\mathcal{G})))$.

In summary, the overall complexity of Algorithm 1 is
$\mathcal{O}(2^{\mathcal{O}(|\varphi|)}\cdot(K^{\varepsilon}+p(\mathcal{G}))+d^{8})$,
which concludes the proof. ∎