经典确定性系统、随机系统的模型检验具有十分重要的意义。在模型检验中,不同种类的可达性定性、定量分析与系统的成功率、安全性、存活性、死锁检验具有十分紧密的联系。因此,可达性分析具有十分重要的地位。量子系统的模型检验同样具有十分重要的意义。其中,可达性分析不仅可以用于验证量子算法、协议的正确性,还可以应用于检验量子设备是否按设计运行。本文主要研究了量子马尔可夫链可达性的定量分析问题与量子马尔可夫决策过程的可达性问题。量子马尔可夫链作为经典马尔可夫链的量子扩展,可以用来刻画已有的大部分量子算法、协议。本文首先扩展量子底层强连通分支的概念,研究其性质以及与经典强连通分支的差异。然后依据这些性质,将量子马尔可夫链的状态空间分解。而后,结合超算子的基本性质,系统解决了量子马尔可夫链可达性、持续可达性、重复可达性的定量分析问题。量子马尔可夫决策过程是经典马尔可夫决策过程的扩展,能够有效刻画大部分离散时间量子系统。本文首先分析了量子马尔可夫决策过程与经典马尔可夫过程、量子马尔可夫链的异同点。而后,给出了其可达性分析中有限步问题的不可判定性。接着,在无限步问题中,证明了一般可达概率的不可计算性,给出了可达概率为1的最优调度程序存在的充分必要条件。最后,给出了量子马尔可夫决策过程可达性分析与联合谱半径、经典系统绝对渐近稳定性之间的关系。