Model Checking Reachability Properties for Quantum Markov Chains

We propose a discrete time quantum Markov chain (QMC) related to previous proposals but yet with a different semantics.
A probability measure is defined similar to as for DTMCs in contrast to e.g.\ the super operator valued measure.
Our work is based on a simple imperative quantum pseudo programming language and its denotational semantics which naturally leads to a definition of a QMC.
As a novelty we demonstrate how reachability events of a QMC expressed in a simple temporal logic like notation may be checked similar to as
for DTMCs as transient state probabilities and how probability intervals of such events may be computed by smallest fixed-point solutions to linear equations.