Checking Continuous Stochastic Logic against Quantum Continuous-Time Markov Chains

TL;DR

This paper develops a symbolic and numerical method for model-checking quantum continuous-time Markov chains against continuous stochastic logic, establishing decidability and efficiency for verifying quantum systems.

Contribution

It introduces an algebraic approach combining projection, matrix exponentiation, and integration for verifying quantum CTMCs against CSL formulas, ensuring decidability and polynomial complexity.

Findings

Decidability of CSL for quantum CTMCs is established.

The method is efficient with polynomial time complexity.

Demonstrated on Apollonian networks as a case study.

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.