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.

翻译：矩阵乘积态（MPS）是一维量子多体系统基态的标准张量网络表示，也是DMRG等广泛使用的模拟工具的基础。然而，尽管量子模型检测主要针对量子程序和通信协议（以时间轴表达性质）已有较成熟发展，但对于物理多体系统的空间依赖性和尺寸依赖性性质——其关键参数为系统尺寸——目前仍缺乏可系统验证的框架。本文旨在弥合这一鸿沟。我们提出线性链逻辑（LCL），这是一种空间逻辑，用于指定周期MPS族随系统尺寸增长的物理意义性质，例如环上的非平凡性和大尺寸渐近模式。我们的方法基于一个简单而强有力的联系：每个周期MPS自然在其虚拟空间上诱导一个完全正映射（量子操作），因此MPS的许多定量特征可以通过该操作的重复应用来分析。利用这一视角，我们推导出一个有效过程，用于计算给定尺寸下MPS的内积，并支持更丰富的LCL规范，无需依赖暴力状态展开。随后，我们开发了结合可靠边界与渐近结构分析的近似模型检测算法，支持对大规模系统的可扩展推理。在代表性MPS族上的实验表明，我们的方法能自动验证非平凡性并检测空间渐近模式，从而与传统数值技术形成互补。