一句话：提出投影、矩阵指数与定积分结合的代数方法，判定并高效模型检测量子CTMC上的CSL公式。
本文研究量子连续时间马尔可夫链（quantum CTMC）的定量模型检测。作者用连续随机逻辑（CSL）刻画其分支时间性质，核心难点在于多阶段 until 路径公式的概率计算。为求解 CSL，他们提出一种代数方法：利用适当投影、矩阵指数和定积分，符号化地计算路径公式的概率测度，从而建立 CSL 的可判定性。为提高效率，进一步引入数值方法，使时间复杂度在输入模型编码规模上为多项式、在公式规模上为线性。最后通过 Apollonian 网络运行实例展示方法。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{XuMGDY25,
title = {Checking Continuous Stochastic Logic against Quantum Continuous-Time Markov Chains},
author = {Ming Xu and Jingyi Mei and Ji Guan and Yuxin Deng and Nengkun Yu},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 4},
year = {2025},
doi = {10.46298/lmcs-21(4:22)2025}
}