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 famous 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的可判定性。为保证计算效率，我们引入数值方法，使得时间复杂度关于输入模型编码规模呈多项式级增长，关于输入公式规模呈线性增长。最后，以阿波罗网络为例演示了该方法的具体应用。