Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Checking Continuous Stochastic Logic against Quantum Continuous-Time Markov Chains

Ming Xu, Jingyi Mei, Ji Guan, Yuxin Deng, Nengkun Yu

TL;DR

The paper addresses verifying CSL properties of quantum continuous-time Markov chains, models that couple a classical subsystem with a quantum subsystem under Lindblad dynamics. It introduces an algebraic, symbolically computable procedure using projection, matrix exponentiation, and definite integration to evaluate multiphase until path probabilities, proving CSL decidability and achieving polynomial-time performance in the model encoding size while acknowledging exponential dependence on qubit count. A numerical speed-up based on scaling and squaring with Padé approximations and Riemann sums is proposed to make the approach practical for larger systems. An Apollonian-network running example demonstrates the method, and an implementation in Mathematica/MATLAB showcases the feasibility of exact and approximate CSL checking on quantum CTMCs, bridging formal verification with open quantum dynamics. The work lays groundwork for future model checking of quantum CTMDPs and highlights the need to address optimization over density operators in quantum settings.

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.

Checking Continuous Stochastic Logic against Quantum Continuous-Time Markov Chains

TL;DR

The paper addresses verifying CSL properties of quantum continuous-time Markov chains, models that couple a classical subsystem with a quantum subsystem under Lindblad dynamics. It introduces an algebraic, symbolically computable procedure using projection, matrix exponentiation, and definite integration to evaluate multiphase until path probabilities, proving CSL decidability and achieving polynomial-time performance in the model encoding size while acknowledging exponential dependence on qubit count. A numerical speed-up based on scaling and squaring with Padé approximations and Riemann sums is proposed to make the approach practical for larger systems. An Apollonian-network running example demonstrates the method, and an implementation in Mathematica/MATLAB showcases the feasibility of exact and approximate CSL checking on quantum CTMCs, bridging formal verification with open quantum dynamics. The work lays groundwork for future model checking of quantum CTMDPs and highlights the need to address optimization over density operators in quantum settings.

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.
Paper Structure (23 sections, 6 theorems, 32 equations, 1 figure, 1 table)

This paper contains 23 sections, 6 theorems, 32 equations, 1 figure, 1 table.

Table of Contents

  1. Introduction
  2. Related Work
  3. Checking on CTMC
  4. Checking on quantum DTMC
  5. Linear-time logic vs branching-time logic
  6. Contribution
  7. Organization
  8. Preliminaries
  9. Quantum Computing
  10. Linear operator
  11. Quantum state
  12. Quantum operation
  13. State evolution
  14. Lindblad Master Equation
  15. Number Theory
  16. ...and 8 more sections

Key Result

Lemma 2.3

Let $\alpha_1$ and $\alpha_2$ be two algebraic numbers of degrees $D_1$ and $D_2$, respectively. There is an algebraic number $\mu$ of degree at most $D_1 D_2$, such that the field extension $\mathbb{Q}(\mu):\mathbb{Q}$ is exactly $\mathbb{Q}(\alpha_1,\alpha_2):\mathbb{Q}$.

Figures (1)

  • Figure 1: The first three generations of ANs

Theorems & Definitions (17)

  • Definition 2.1
  • Definition 2.2
  • Lemma 2.3: Loo83
  • Lemma 2.4: Coh93
  • Theorem 2.5: (Lindemann 1882) Bak75
  • Definition 3.1
  • Lemma 3.2: XMG+21
  • Example 3.3
  • Definition 3.4
  • Example 3.5
  • ...and 7 more