Model Checking Matrix Product States against Linear Chain Logic

TL;DR

This paper introduces Linear Chain Logic (LCL), a new framework for verifying size-dependent properties of matrix product states in quantum many-body systems, enabling scalable analysis of large systems.

Contribution

It proposes LCL for specifying properties of MPS as system size grows and develops scalable model-checking algorithms based on quantum operations.

Findings

Effective procedure for computing MPS inner products at given sizes

Approximate model-checking algorithms combining bounding and structural analysis

Automatic verification of nontriviality and asymptotic spatial regimes in MPS

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.