Measuring the constrained reachability in quantum Markov chains

Constrained reachability is a kind of quantitative path property, which is generally specified by multiphase until formulas originated in continuous stochastic logic. In this paper, through proposing a positive operator valued measure on the set of infinite paths, we develop an exact method to solve the constrained reachability problem for quantum Markov chains. The convergence rate of the reachability is also obtained. We then analyse the complexity of the proposed method, which turns out to be in polynomial-time w.r.t. the size of the classical state space and the dimension of the accompanied Hilbert space. Finally, our method is implemented and applied to a simple quantum protocol.