  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.
