Reachability Analysis Of Quantum Markov Chains And Markov Decision Processes

Reachability analysis is strongly related to the analysis of success probability, safety property, liveness property, and deadlock detection. Therefore it plays an important role in model checking of classical deterministic and probabilistic systems.As well, model checking of quantum systems, especially reachability analysis, plays a very important role in verifying the correctness of quantum algorithms and protocols,and the realization of quantum equipments. We analyze the quantitative reachability problems of quantum Markov chains and the reachability problems of quantum Markov decision processes.As a quantum generalization of classical Markov chain, quantum Markov chain can be employed to formalize most quantum algorithms and protocols. We first generalize the notion of quantum bottom strongly connected component, and develop its properties, and then employ these properties to decompose the state space of a quantum Markov chain.Therefore the quantitative analysis of reachability, repeated reachability and persistence property of quantum Markov chains can be solved by employing the decomposition and the basic properties of super-operators.Quantum Markov decision process is a quantum generalization of classical Markov decision process, and can be used to model most discrete-time quantum systems. We first focus on the difference between quantum Markov decision processes and classical Markov decision processes, as well as quantum Markov chains. And then we present some undecidability on finite-horizon problems in the reachability analysis. Meanwhile we prove the general supremum reachability probability of quantum Markov decision processes is uncomputable, and then present the necessary and sufficient condition for the existence of an optimal scheduler with reachability probability 1. Finally we give the relationship between reachability analysis and joint spectral radius, which is strongly related to the absolute asymptotic stability of classical discrete linear systems.