Model Checking Matrix Product States against Linear Chain Logic

• URL: http://arxiv.org/abs/2605.14356v1
• Date: Thu, 14 May 2026 04:33:59 GMT
• Title: Model Checking Matrix Product States against Linear Chain Logic
• Abstract summary: Matrix product states (MPS) are a standard tensor-network representation for ground states of one-dimensional quantum many-body systems.<n>There is still no comparable framework for systematically verifying emphspatial and emphsize-dependent properties of physical many-body states.
• Score: 9.230090345117846
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Matrix product states (MPS) are a standard tensor-network representation for ground states of one-dimensional quantum many-body systems, and they underpin widely used simulation tools such as DMRG. However, while quantum model checking has been developed mainly for quantum programs and communication protocols (with properties expressed along a time axis), there is still no comparable framework for systematically verifying \emph{spatial} and \emph{size-dependent} properties of physical many-body states, where the key parameter is the system size. This paper takes a step toward bridging the gap. We propose \emph{Linear Chain Logic} (LCL), a spatial logic designed to specify physically meaningful properties of periodic MPS families as the system size grows, such as nontriviality on rings and large-size asymptotic patterns. Our approach builds on a simple but powerful connection: every periodic MPS naturally induces a completely positive map (a quantum operation) on its virtual space, so many quantitative features of the MPS can be analysed through the repeated application of the operation. Using this perspective, we derive an effective procedure to compute the inner products of an MPS at a given size and to support richer LCL specifications, without relying on brute-force state expansion. We then develop approximate model-checking algorithms that combine sound bounding with asymptotic structural analysis, enabling scalable reasoning about large system sizes. Experiments on representative MPS families illustrate that our method can automatically verify nontriviality and detect asymptotic spatial regimes in a way that complements traditional numerical techniques.

Related papers

• Large Scale Entanglement Structure Detection in 100-Qubit Systems via Local Joint Measurements [38.19492379134641]
  We introduce a scalable framework that recognizes large-scale entanglement structures directly from local correlation fingerprints.<n>In noisy simulations, this protocol classifies GHZ-, W-, and cluster-type structures among 30 candidate partitions with a mean accuracy exceeding 95%.<n>We further validate the protocol on a superconducting quantum processor, where it reliably classifies block structures for systems of up to 13 qubits.
  arXiv  Detail & Related papers  (2026-08-20T15:25:03Z)
• State Diagnostics of Complexity in Open Quantum Systems [39.146761527401424]
  We study the emergence of complexity in finite-size quantum systems.<n>We represent mixed quantum states as probability measures on complex projective Hilbert space.
  arXiv  Detail & Related papers  (2026-08-10T15:09:52Z)
• Statistical and Algorithmic Foundations of Probing Quantum Systems with Compressive Measurements: A Review [23.123362765639214]
  Quantum state tomography aims to reconstruct unknown quantum states from measurement data.<n>Prior structure, such as low-rankness, tensor-network representations, shallow quantum circuits, and neural quantum states, can substantially reduce the effective degrees of freedom.
  arXiv  Detail & Related papers  (2026-05-26T15:44:42Z)
• Online Riemannian Gradient Descent for Quantum State Tomography with Matrix Product Operators [8.817652993229068]
  Matrix product operators (MPOs) provide a scalable approach for quantum state tomography (QST)<n>We study QST for quantum density matrices that can be represented by MPOs.<n>Motivated by this formulation, we develop an online gradient descent (oRGD) algorithm that sequentially incorporates measurement data.
  arXiv  Detail & Related papers  (2026-05-06T06:19:46Z)
• Efficient Learning Algorithms for Noisy Quantum State and Process Tomography [17.414887413731385]
  We introduce a provably efficient and structure-agnostic learning framework for noisy $n$-qubit quantum circuits.<n>Results provide a scalable and practically relevant route toward characterizing large-scale noisy quantum devices.
  arXiv  Detail & Related papers  (2026-03-02T06:50:59Z)
• Efficient time-evolution of matrix product states using average Hamiltonians [0.0]
  We propose a simple, yet efficient, method to augment the already available MPS algorithms to simulate the dynamics of time-dependent Hamiltonians.<n>Our work paves the way for efficient simulation of QMBS under the influence of time-dependent Hamiltonians.
  arXiv  Detail & Related papers  (2026-02-04T19:00:01Z)
• Unified Framework for Direct Characterization of Kraus Operators, Observables, Density Matrices, and Weak Values Without Weak Interaction [0.007186737422124123]
  Generalized quantum measurements are essential for modeling realistic processes in open quantum systems.<n>While quantum process tomography can fully characterize a POVM, it is resource-intensive and impractical when only specific POVM elements are of interest.<n>Direct quantum measurement tomography offers a more efficient alternative but typically relies on weak interactions and complex structures of the system.
  arXiv  Detail & Related papers  (2025-10-08T17:40:07Z)
• Contraction, Criticality, and Capacity: A Dynamical-Systems Perspective on Echo-State Networks [13.857230672081489]
  We present a unified, dynamical-systems treatment that weaves together functional analysis, random attractor theory and recent neuroscientific findings.<n>First, we prove that the Echo-State Property (wash-out of initial conditions) together with global Lipschitz dynamics necessarily yields the Fading-Memory Property.<n>Second, employing a Stone-Weierstrass strategy we give a streamlined proof that ESNs with nonlinear reservoirs and linear read-outs are dense in the Banach space of causal, time-in fading-memory filters.<n>Third, we quantify computational resources via memory-capacity spectrum, show how
  arXiv  Detail & Related papers  (2025-07-24T14:41:18Z)
• Generating Generalised Ground-State Ansatzes from Few-Body Examples [0.0]
  We introduce a method that generates ground-state ansatzes for quantum many-body systems.<n>We find analytically tractable ansatzes with a degree of universality, which encode correlations, capture finite-size effects, accurately predict ground-state energies, and offer a good description of critical phenomena.
  arXiv  Detail & Related papers  (2025-03-01T13:52:57Z)
• Sample-Efficient Quantum State Tomography for Structured Quantum States in One Dimension [25.333797381352973]
  Many physical quantum states often exhibit certain low-dimensional structures that enable the development of efficient QST.<n>We show that the number of state copies to guarantee bounded recovery error of an MPO state with a constrained least-squares estimator depends on the probability distribution of the MPO.<n>We prove that only a number of state copies proportional to the number of independent parameters in the MPO is sufficient for a guaranteed recovery of any state represented by an MPO.
  arXiv  Detail & Related papers  (2024-10-03T15:26:26Z)
• End-to-end resource analysis for quantum interior point methods and portfolio optimization [63.4863637315163]
  We provide a complete quantum circuit-level description of the algorithm from problem input to problem output. We report the number of logical qubits and the quantity/depth of non-Clifford T-gates needed to run the algorithm.
  arXiv  Detail & Related papers  (2022-11-22T18:54:48Z)
• Fixed Depth Hamiltonian Simulation via Cartan Decomposition [59.20417091220753]
  We present a constructive algorithm for generating quantum circuits with time-independent depth. We highlight our algorithm for special classes of models, including Anderson localization in one dimensional transverse field XY model. In addition to providing exact circuits for a broad set of spin and fermionic models, our algorithm provides broad analytic and numerical insight into optimal Hamiltonian simulations.
  arXiv  Detail & Related papers  (2021-04-01T19:06:00Z)
• Analysis of a density matrix renormalization group approach for transport in open quantum systems [0.0]
  Density matrix renormalization group-based tools have been widely used in the study of closed systems. We present an implementation based on state-of-the-art matrix product state (MPS) and tensor network methods. We show that this implementation is suited for studying thermal transport in one-dimensional systems.
  arXiv  Detail & Related papers  (2020-09-17T10:37:49Z)
• Holographic quantum algorithms for simulating correlated spin systems [0.0]
  We present a suite of "holographic" quantum algorithms for efficient ground-state preparation and dynamical evolution of correlated spin-systems. The algorithms exploit the equivalence between matrix-product states (MPS) and quantum channels, along with partial measurement and qubit re-use. As a demonstration of the potential resource savings, we implement a holoVQE simulation of the antiferromagnetic Heisenberg chain on a trapped-ion quantum computer.
  arXiv  Detail & Related papers  (2020-05-06T18:00:01Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.