Checking Continuous Stochastic Logic against Quantum Continuous-Time Markov Chains

Logical Methods in Computer Science, vol. Volume 21, Issue 4

Abstract

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.

Authors 5

1. Ming Xu

   Shanghai Key Laboratory of Trustworthy Computing · Shanghai Qi Zhi Institute · East China Normal University

   Affiliation as printed

   Shanghai Key Lab of Trustworthy Computing , East China Normal University , China, &

   Shanghai Qi Zhi Institute , China

2. Jingyi Mei

   Shanghai Key Laboratory of Trustworthy Computing · East China Normal University

   Affiliation as printed

   Shanghai Key Lab of Trustworthy Computing , East China Normal University , China , & Leiden Institute of Advanced Computer Science ,

3. Ji Guan

   Chinese Academy of Sciences

   Affiliation as printed

   Key Laboratory of System Software (Chinese Academy of Sciences) &

4. Yuxin Deng Aachen

   Leiden University · Shanghai University of Finance and Economics

   Affiliation as printed

   Leiden University , The Netherlands

   MoE Key Laboratory of Interdisciplinary Research of Computation and Economics , Shanghai University of Finance and Economics , China

5. Nengkun Yu

   Stony Brook University

   Affiliation as printed

   Department of Computer Science , Stony Brook University , United States