论文标题
检查连续的随机逻辑与量子连续时间马尔可夫链
Checking Continuous Stochastic Logic against Quantum Continuous-Time Markov Chains
论文作者
论文摘要
在过去的几十年中，验证量子系统引起了很大的兴趣。在本文中，我们研究了量子连续时间马尔可夫链（量子CTMC）的定量模型检查。量子CTMC的分支时间特性由连续随机逻辑（CSL）指定，该逻辑（CSL）众所周知，用于验证包括经典CTMC在内的实时系统。检查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.
