Verifying quantum systems has attracted a lot of interest in the last decades.In this paper, we study the quantitative model-checking of quantum continuous-time Markov chains (quantum CTMCs). The branching-time properties of quantum CTMCs are specified by continuous stochastic logic (CSL), which is well-known for verifying real-time systems, including classical CTMCs. The core of checking the CSL formulas lies in tackling multiphase until formulas. We develop an algebraic method using proper projection, matrix exponentiation, and definite integration to symbolically calculate the probability measures of path formulas. Thus the decidability of CSL is established. To be efficient, numerical methods are incorporated to guarantee that the time complexity is polynomial in the encoding size of the input model and linear in the size of the input formula. A running example of Apollonian networks is further provided to demonstrate our method.

翻译：在过去的几十年中，量子系统的验证引起了广泛关注。本文研究了量子连续时间马尔可夫链（量子CTMC）的定量模型检验问题。量子CTMC的分支时间性质由连续随机逻辑（CSL）描述，该逻辑在实时系统（包括经典CTMC）验证中已广为人知。检验CSL公式的核心在于处理多阶段until公式。我们发展了一种代数方法，利用恰当投影、矩阵指数运算和定积分，以符号化方式计算路径公式的概率测度，从而确立了CSL的可判定性。为提高效率，我们结合数值方法，确保算法时间复杂度在输入模型编码规模上为多项式级，在输入公式规模上为线性级。文中进一步以阿波罗网络为例演示了所提方法。