Ming Xu ; Jingyi Mei ; Ji Guan ; Yuxin Deng ; Nengkun Yu - Checking Continuous Stochastic Logic against Quantum Continuous-Time Markov Chains

lmcs:9077 - Logical Methods in Computer Science, November 11, 2025, Volume 21, Issue 4 - https://doi.org/10.46298/lmcs-21(4:22)2025
Checking Continuous Stochastic Logic against Quantum Continuous-Time Markov ChainsArticle

Authors: Jingyi Mei ; Ming Xu ; Ji Guan ; Yuxin Deng ; Nengkun Yu

    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.


    Volume: Volume 21, Issue 4
    Published on: November 11, 2025
    Accepted on: September 16, 2025
    Submitted on: February 14, 2022
    Keywords: Logic in Computer Science

    Consultation statistics

    This page has been seen 296 times.
    This article's PDF has been downloaded 140 times.