Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Model Checking Quantum Continuous-Time Markov Chains

Ming Xu, Jingyi Mei, Ji Guan, Nengkun Yu

TL;DR

This work addresses verification of quantum real-time systems by introducing quantum continuous-time Markov chains (QCTMC) and specifying properties in signal temporal logic (STL). It develops an exact STL model-checking framework based on real root isolation of exponential polynomials, leveraging Schanuel's conjecture for completeness, and uses interval operations to handle general STL formulas with linear complexity in formula size. The paper defines the QCTMC formalism, connects it to classical CTMCs, and demonstrates the approach on an open quantum walk with absorbing boundaries. Under the conjectural assumptions, STL becomes decidable for QCTMCs, enabling rigorous and scalable verification of quantum real-time behavior with practical running examples and a clear computational pipeline.

Abstract

Verifying quantum systems has attracted a lot of interests in the last decades. In this paper, we initialised the model checking of quantum continuous-time Markov chain (QCTMC). As a real-time system, we specify the temporal properties on QCTMC by signal temporal logic (STL). To effectively check the atomic propositions in STL, we develop a state-of-art real root isolation algorithm under Schanuel's conjecture; further, we check the general STL formula by interval operations with a bottom-up fashion, whose query complexity turns out to be linear in the size of the input formula by calling the real root isolation algorithm. A running example of an open quantum walk is provided to demonstrate our method.

Model Checking Quantum Continuous-Time Markov Chains

TL;DR

This work addresses verification of quantum real-time systems by introducing quantum continuous-time Markov chains (QCTMC) and specifying properties in signal temporal logic (STL). It develops an exact STL model-checking framework based on real root isolation of exponential polynomials, leveraging Schanuel's conjecture for completeness, and uses interval operations to handle general STL formulas with linear complexity in formula size. The paper defines the QCTMC formalism, connects it to classical CTMCs, and demonstrates the approach on an open quantum walk with absorbing boundaries. Under the conjectural assumptions, STL becomes decidable for QCTMCs, enabling rigorous and scalable verification of quantum real-time behavior with practical running examples and a clear computational pipeline.

Abstract

Verifying quantum systems has attracted a lot of interests in the last decades. In this paper, we initialised the model checking of quantum continuous-time Markov chain (QCTMC). As a real-time system, we specify the temporal properties on QCTMC by signal temporal logic (STL). To effectively check the atomic propositions in STL, we develop a state-of-art real root isolation algorithm under Schanuel's conjecture; further, we check the general STL formula by interval operations with a bottom-up fashion, whose query complexity turns out to be linear in the size of the input formula by calling the real root isolation algorithm. A running example of an open quantum walk is provided to demonstrate our method.

Paper Structure

This paper contains 11 sections, 8 theorems, 17 equations, 2 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. Organisation
  3. Preliminaries
  4. Quantum Computing
  5. Lindblad's Master Equation
  6. Number Theory
  7. Quantum Continuous-Time Markov Chain
  8. Signal Temporal Logic
  9. Solving Atomic Propositions
  10. Checking STL Formulas
  11. Concluding Remarks

Key Result

Lemma 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 (2)

  • Figure 2: Flow chart of the whole isolation procedure
  • Figure 3: Parse tree of the STL formula $\phi_1$

Theorems & Definitions (19)

  • Definition 1
  • Definition 2
  • Lemma 3: Loo83
  • Lemma 4: Coh96
  • Theorem 5: Lindemann (1882) Bak75
  • Conjecture 6: Schanuel (1960s) Ax71
  • Corollary 7: COW16
  • Definition 8
  • Definition 9
  • Lemma 10
  • ...and 9 more