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.
翻译:校验量量子系统在过去几十年中吸引了许多人的兴趣。 在本文中, 我们研究了量子连续时间 Markov 链( Qantom CTMCs) 的定量模型检查。 量子连续时间 Markov 链( Quantum CTMCs) 的分流时间特性由连续的随机逻辑( CSL) 来指定, 该逻辑在实时系统( 包括古典 CTMCs) 的校验中很出名。 校验 CSL 公式的核心在于处理多阶段直到公式。 我们开发了一种代数方法, 使用正确的投影、 矩阵缩放和 明确整合来象征性地计算路径公式的概率 。 因此, CLSL 的可变性已经建立 。 为了高效, 将数字方法纳入, 以保证输入模型的编码尺寸和输入公式大小的线性的时间复杂性是多元的。 提供了阿波罗尼亚 网络的运行示例, 以演示我们的方法 。