Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Image Computation for Quantum Transition Systems

Xin Hong, Dingchao Gao, Sanjiang Li, Shenggang Ying, Mingsheng Ying

TL;DR

The paper addresses the challenge of verification for quantum transition systems by introducing efficient image computation methods that treat quantum circuits as tensor networks and use tensor decision diagrams. It develops a basic image computation algorithm and two partition-based optimisations—addition and contraction partitions—to mitigate the inherent hardness of tensor contractions. Empirical results show that contraction partition dramatically improves efficiency, enabling scalable analysis of circuits such as BV, GHZ, Grover, QFT, and QRW with hundreds of qubits. The work advances practical quantum hardware verification and provides a framework for scalable, tensor-network-based model checking in quantum domains.

Abstract

With the rapid progress in quantum hardware and software, the need for verification of quantum systems becomes increasingly crucial. While model checking is a dominant and very successful technique for verifying classical systems, its application to quantum systems is still an underdeveloped research area. This paper advances the development of model checking quantum systems by providing efficient image computation algorithms for quantum transition systems, which play a fundamental role in model checking. In our approach, we represent quantum circuits as tensor networks and design algorithms by leveraging the properties of tensor networks and tensor decision diagrams. Our experiments demonstrate that our contraction partition-based algorithm can greatly improve the efficiency of image computation for quantum transition systems.

Image Computation for Quantum Transition Systems

TL;DR

The paper addresses the challenge of verification for quantum transition systems by introducing efficient image computation methods that treat quantum circuits as tensor networks and use tensor decision diagrams. It develops a basic image computation algorithm and two partition-based optimisations—addition and contraction partitions—to mitigate the inherent hardness of tensor contractions. Empirical results show that contraction partition dramatically improves efficiency, enabling scalable analysis of circuits such as BV, GHZ, Grover, QFT, and QRW with hundreds of qubits. The work advances practical quantum hardware verification and provides a framework for scalable, tensor-network-based model checking in quantum domains.

Abstract

With the rapid progress in quantum hardware and software, the need for verification of quantum systems becomes increasingly crucial. While model checking is a dominant and very successful technique for verifying classical systems, its application to quantum systems is still an underdeveloped research area. This paper advances the development of model checking quantum systems by providing efficient image computation algorithms for quantum transition systems, which play a fundamental role in model checking. In our approach, we represent quantum circuits as tensor networks and design algorithms by leveraging the properties of tensor networks and tensor decision diagrams. Our experiments demonstrate that our contraction partition-based algorithm can greatly improve the efficiency of image computation for quantum transition systems.

Paper Structure

This paper contains 20 sections, 1 theorem, 4 equations, 5 figures, 2 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Background
  3. Quantum State Space and Quantum Operations
  4. Tensor Decision Diagram
  5. Quantum Transition Systems
  6. Modelling Quantum Circuits
  7. Combinational Quantum Circuits
  8. Dynamic Quantum Circuits
  9. Noisy quantum circuits
  10. Basic Algorithms
  11. Representation of Subspaces
  12. Computing the Join of Two Subspaces
  13. A Basic Image Computation Algorithm
  14. Partition-Based Optimisations
  15. Addition Partition
  16. ...and 5 more sections

Key Result

Proposition 1

Let $\mathcal{T}$ be a quantum operation. Then

Figures (5)

  • Figure 1: A matrix $P$ and its TDD representation. Note that edges with weight 0 are omitted in this diagram.
  • Figure 2: The circuit for Grover iteration. It is also a tensor network with indices $x^j_i$, which denotes the $j$-th index on qubit $i$.
  • Figure 3: The circuit for correcting one qubit bit-flip error.
  • Figure 4: A noisy version of a quantum walk along a 8-length cycle.
  • Figure 5: The undirected graph for Grover iteration (cf. Fig. \ref{['fig:cir_grover']}), where $x_i^j$ represents the $j$-th index of the $i$-th qubit of the circuit.

Theorems & Definitions (5)

  • Definition 1
  • Proposition 1: Ying21mcqsbook
  • Definition 2
  • Example 1
  • Example 2