Model Checking Matrix Product States against Linear Chain Logic

Ji Guan; Ming Xu; Yihao Chen

REVIEW 2 major objections 2 minor 47 references

Linear Chain Logic verifies spatial and size-dependent properties of periodic matrix product states by iterating induced completely positive maps.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.3

2026-06-30 20:55 UTC pith:GNJU7LIV

load-bearing objection The paper defines Linear Chain Logic for spatial MPS properties and reduces checks to CP-map iteration on the virtual space, with approximate algorithms for large sizes. the 2 major comments →

arxiv 2605.14356 v1 pith:GNJU7LIV submitted 2026-05-14 quant-ph cs.LO

Model Checking Matrix Product States against Linear Chain Logic

Ming Xu , Yihao Chen , Ji Guan This is my paper

classification quant-ph cs.LO

keywords matrix product stateslinear chain logicmodel checkingcompletely positive mapsquantum many-body systemsspatial propertiestensor networksasymptotic analysis

verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces Linear Chain Logic as a spatial logic for expressing properties of families of periodic matrix product states that change with system size. It establishes that each such state induces a completely positive map on virtual space, so repeated application of the map encodes quantitative spatial features. Procedures follow for computing inner products at fixed sizes and for approximate model checking that combines bounding with asymptotic analysis. A reader would care because this supplies a verification method for many-body states where brute-force expansion becomes impossible as size grows.

Core claim

Every periodic MPS induces a completely positive map on its virtual space, and repeated application of this map supports an effective procedure to compute inner products together with approximate model-checking algorithms for Linear Chain Logic specifications such as nontriviality on rings and large-size asymptotic patterns.

What carries the argument

The completely positive map induced by a periodic MPS on its virtual space, whose iterations capture the spatial features required by LCL specifications.

Load-bearing premise

Every periodic MPS induces a completely positive map whose repeated application captures the quantitative spatial features needed for LCL specifications.

What would settle it

A concrete periodic MPS family where the inner-product or model-checking procedure returns a result that directly contradicts the value obtained by explicit contraction at moderate system sizes.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

Inner products between two periodic MPS can be obtained at any chosen system size without expanding the full state.
LCL specifications that include nontriviality on rings become decidable through the map iteration.
Approximate algorithms combining sound bounds and asymptotic analysis scale to system sizes where direct methods fail.
Detection of large-size asymptotic spatial regimes is automated for representative MPS families.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same map-iteration technique could be tested on MPS that approximate ground states of specific Hamiltonians to check consistency with known phase diagrams.
Extension to open-boundary or non-periodic MPS would require a different map construction but might reuse the bounding and asymptotic parts of the algorithms.
Integration with existing DMRG output could allow automatic post-processing of computed states for LCL properties.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Desk Editor's Note

The paper defines Linear Chain Logic for spatial MPS properties and reduces checks to CP-map iteration on the virtual space, with approximate algorithms for large sizes.

read the letter

The main thing here is a new spatial logic LCL aimed at periodic MPS families, plus a reduction that turns verification into repeated application of the transfer map viewed as a CP operation. That lets them compute inner products at fixed size and handle asymptotic patterns without expanding the full chain.

What works is the basic move: MPS transfer operators already encode spatial correlations, so folding that into a logic for nontriviality on rings or large-size regimes is a reasonable step. The approximate model-checking part, mixing bounds with asymptotic analysis, looks practical for avoiding brute force on big systems. Experiments on representative families show it can flag the intended properties.

The soft spot is that the CP-map connection is the standard transfer-operator fact from the MPS literature, so the lift to model checking is the real increment rather than a fresh technical insight. The abstract and description give no derivations or error bounds, which makes it hard to judge how sound the approximations stay when the logic gets more complex. If the full proofs are just re-packaging existing contraction arguments, the advance stays modest.

This is for people already working at the intersection of tensor networks and formal verification. It is coherent enough on its own terms to go to a serious referee, though the bar for acceptance will be whether the logic definitions and algorithms add enough beyond the transfer map to justify a new framework.

Referee Report

2 major / 2 minor

Summary. The paper introduces Linear Chain Logic (LCL), a spatial logic for specifying size-dependent and asymptotic properties of periodic matrix product states (MPS) families, such as nontriviality on rings. It establishes that every periodic MPS induces a completely positive map on its virtual space, uses this to derive an effective procedure for inner-product computation at fixed size and for supporting LCL specifications without brute-force expansion, develops approximate model-checking algorithms combining bounding and asymptotic analysis, and illustrates the approach via experiments on representative MPS families.

Significance. If the central constructions and algorithms are correct, the work supplies a new verification framework that connects tensor-network representations to spatial model checking, enabling scalable reasoning about physically relevant properties of MPS that complement existing numerical techniques such as DMRG. The explicit link to completely positive maps and the provision of both exact and approximate procedures are concrete strengths.

major comments (2)

[§3] §3 (Connection to CP maps): the claim that repeated application of the induced CP map captures all quantitative spatial features required by LCL specifications is stated at a high level; a concrete derivation showing how an arbitrary LCL formula reduces to an expression involving iterates of the transfer map (or its Kraus operators) is needed to confirm that the reduction is effective and does not introduce hidden exponential cost.
[§4.2] §4.2 (Approximate model checking): the soundness argument for the bounding procedure relies on an asymptotic structural analysis whose error term is not quantified; without an explicit bound relating the truncation depth to the LCL formula size and the spectral gap of the CP map, it is unclear whether the method remains sound for the full class of LCL formulas when system size tends to infinity.

minor comments (2)

[Abstract] The abstract and introduction use the phrase 'effective procedure' without clarifying whether it is polynomial-time in the MPS bond dimension or merely decidable; a complexity statement would strengthen the claims.
[§2] Notation for the virtual-space CP map (e.g., the symbol used for the transfer operator) is introduced without an explicit comparison table to the standard MPS transfer matrix E; adding such a table would aid readers familiar with the DMRG literature.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their thorough review and valuable suggestions. We address each of the major comments below and outline the revisions we will make to the manuscript.

read point-by-point responses

Referee: [§3] §3 (Connection to CP maps): the claim that repeated application of the induced CP map captures all quantitative spatial features required by LCL specifications is stated at a high level; a concrete derivation showing how an arbitrary LCL formula reduces to an expression involving iterates of the transfer map (or its Kraus operators) is needed to confirm that the reduction is effective and does not introduce hidden exponential cost.

Authors: We acknowledge that the connection in §3 is presented at a high level in the current manuscript. To address this, we will add a detailed derivation in the revised version, explicitly showing the inductive reduction of arbitrary LCL formulas to expressions involving iterates of the transfer map and its Kraus operators. This will demonstrate that the procedure is effective and avoids hidden exponential costs by leveraging the structure of the CP map. revision: yes
Referee: [§4.2] §4.2 (Approximate model checking): the soundness argument for the bounding procedure relies on an asymptotic structural analysis whose error term is not quantified; without an explicit bound relating the truncation depth to the LCL formula size and the spectral gap of the CP map, it is unclear whether the method remains sound for the full class of LCL formulas when system size tends to infinity.

Authors: The referee is correct that the error term requires explicit quantification for full rigor. In the revision, we will include a precise bound on the truncation error in terms of the depth, the size of the LCL formula, and the spectral gap of the CP map. This will establish soundness for all LCL formulas in the asymptotic regime. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained

full rationale

The paper proposes LCL as a new spatial logic and builds an analysis procedure on the standard fact that periodic MPS induce CP maps via the transfer operator. No equations, fitted parameters, or self-citations are shown reducing any central claim to a definition or prior result by the same authors. The inner-product computation and model-checking algorithms follow directly from the known MPS transfer map without internal reduction to inputs. This matches the default expectation of no circularity.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claim rests on the existence of the LCL semantics and the soundness of the reduction to CP-map iteration; no free parameters, ad-hoc axioms, or invented physical entities are mentioned in the abstract.

axioms (1)

domain assumption Every periodic MPS induces a completely positive map on its virtual space whose iteration encodes the spatial properties of the state.
Invoked in the abstract paragraph that links MPS to CP maps and states that many quantitative features can be analysed through repeated application.

invented entities (1)

Linear Chain Logic (LCL) no independent evidence
purpose: Spatial logic for specifying nontriviality on rings and asymptotic patterns of periodic MPS families.
Newly proposed in the paper; no independent evidence supplied in abstract.

pith-pipeline@v0.9.1-grok · 5787 in / 1318 out tokens · 21108 ms · 2026-06-30T20:55:18.609381+00:00 · methodology

0 comments

read the original 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.

Figures

Figures reproduced from arXiv: 2605.14356 by Ji Guan, Ming Xu, Yihao Chen.

**Figure 1.** Figure 1: Schematic overview of a 1D quantum many-body system and its MPS. Problem 1 (MPS Nonzeroness Dichotomy). Given a set of matrices {Ak} d k=1 ⊂ C D×D defining |ψN ⟩ in (4) and an integer J ≥ 1, decide: – (Always-nonzero after J) Does |ψN ⟩ ̸= 0 hold for all N ≥ J? – (Ultimately nonzero) Does there exist N0 ≥ J such that |ψN ⟩ ̸= 0 holds for all N ≥ N0? Physical meaning. Problem 1 asks whether a fixed local te… view at source ↗

discussion (0)

Reference graph

Works this paper leans on

47 extracted references · 47 canonical work pages · 5 internal anchors

[1]

Clarke, Orna Grumberg, and Doron A

Edmund M. Clarke, Orna Grumberg, and Doron A. Peled.Model Checking. MIT Press, 1999

work page 1999
[2]

MIT Press, 2008

Christel Baier and Joost-Pieter Katoen.Principles of Model Checking. MIT Press, 2008

work page 2008
[3]

Model-checking quantum systems.National Science Review, 6(1):28–31, 2019

Mingsheng Ying and Yuan Feng. Model-checking quantum systems.National Science Review, 6(1):28–31, 2019

work page 2019
[4]

Cambridge University Press, 2021

Mingsheng Ying and Yuan Feng.Model Checking Quantum Systems: Principles and Algorithms. Cambridge University Press, 2021

work page 2021
[5]

Michael M. Wolf. Quantum channels & operations: Guided tour. Lecture notes available athttps://www-m5.ma.tum.de/foswiki/pub/M5/Allgemeines/ MichaelWolf/QChannelLecture.pdf, 2012

work page 2012
[6]

Daniel A. Lidar. Review of decoherence free subspaces, noiseless subsys- tems, and dynamical decoupling.arXiv, abs/1208.5791, 2012. available at https://arxiv.org/abs/1208.5791

work page internal anchor Pith review Pith/arXiv arXiv 2012
[7]

The Structure of Decoherence-free Subsystems

Ji Guan, Yuan Feng, and Mingsheng Ying. The structure of decoherence-free subsystems.arXiv, abs/1802.04904, 2018. available at https://arxiv.org/abs/1802.04904

work page internal anchor Pith review Pith/arXiv arXiv 2018
[8]

Morgan Kaufmann, 2 edition, 2024

Mingsheng Ying.Foundations of Quantum Programming. Morgan Kaufmann, 2 edition, 2024

work page 2024
[9]

Springer, 2019

Bei Zeng, Xie Chen, Duan-Lu Zhou, and Xiao-Gang Wen.Quantum Information Meets Quantum Matter: From Quantum Entanglement to Topological Phase of Many-Body Systems. Springer, 2019

work page 2019
[10]

Regular language quantum states

Marta Florido-Llin` as, ´Alvaro M. Alhambra, David P´ erez-Garc´ ıa, and J. Ignacio Cirac. Regular language quantum states.arXiv, abs/2407.17641, 2024. available at https://arxiv.org/abs/2407.17641

work page internal anchor Pith review Pith/arXiv arXiv 2024
[11]

The density-matrix renormalization group in the age of matrix product states.Annals of Physics, 326(1):96–192, 2011

Ulrich Schollw¨ ock. The density-matrix renormalization group in the age of matrix product states.Annals of Physics, 326(1):96–192, 2011

work page 2011
[12]

Hastings

Matthew B. Hastings. An area law for one-dimensional quantum systems.Journal of Statistical Mechanics: Theory and Experiment, 2007(08):P08024, 2007

work page 2007
[13]

Vazirani

Dorit Aharonov, Itai Arad, Zeph Landau, and Umesh V. Vazirani. The 1d area law and the complexity of quantum states: A combinatorial approach. InIEEE 52nd Annual Symposium on Foundations of Computer Science, FOCS 2011, pages 324–333. IEEE Computer Society, 2011

work page 2011
[14]

Clarke, E

Edmund M. Clarke, E. Allen Emerson, and A. Prasad Sistla. Automatic verifica- tion of finite-state concurrent systems using temporal logic specifications.ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986

work page 1986
[15]

Model checking quantum Markov chains.Journal of Computer and System Sciences, 79(7):1181–1198, 2013

Yuan Feng, Nengkun Yu, and Mingsheng Ying. Model checking quantum Markov chains.Journal of Computer and System Sciences, 79(7):1181–1198, 2013

work page 2013
[16]

Model Checking Quantum Systems --- A Survey

Mingsheng Ying and Yuan Feng. Model checking quantum systems — A survey. arXiv, abs/1807.09466, 2018. available at https://arxiv.org/abs/1807.09466

work page internal anchor Pith review Pith/arXiv arXiv 2018
[17]

A practical introduction to tensor networks: Matrix product states and projected entangled pair states.Annals of Physics, 349:117–158, 2014

Rom´ an Or´ us. A practical introduction to tensor networks: Matrix product states and projected entangled pair states.Annals of Physics, 349:117–158, 2014

work page 2014
[18]

Wolf, and J

David P´ erez-Garc´ ıa, Frank Verstraete, Michael M. Wolf, and J. Ignacio Cirac. Matrix product state representations.Quantum Information & Computation, 7(5):401–430, 2007

work page 2007
[19]

Mark Fannes, Bruno Nachtergaele, and Reinhard F. Werner. Finitely corre- lated states on quantum spin chains.Communications in Mathematical Physics, 144(3):443–490, 1992. 21

work page 1992
[20]

Nielsen and Isaac L

Michael A. Nielsen and Isaac L. Chuang.Quantum Computation and Quantum Information. Cambridge University Press, 2000

work page 2000
[21]

Ignacio Cirac, David Perez-Garcia, Norbert Schuch, and Frank Verstraete

J. Ignacio Cirac, David Perez-Garcia, Norbert Schuch, and Frank Verstraete. Ma- trix product states and projected entangled pair states: Concepts, symmetries, theorems.Reviews of Modern Physics, 93(4):045003, 2021

work page 2021
[22]

Ignacio Cirac, Norbert Schuch, and David Perez-Garcia

Gemma De las Cuevas, J. Ignacio Cirac, Norbert Schuch, and David Perez-Garcia. Irreducible forms of matrix product states: Theory and applications.Journal of Mathematical Physics, 58(12):121901, 2017

work page 2017
[23]

Completely positive linear maps on complex matrices.Linear Algebra and Its Applications, 10(3):285–290, 1975

Man-Duen Choi. Completely positive linear maps on complex matrices.Linear Algebra and Its Applications, 10(3):285–290, 1975

work page 1975
[24]

Prentice-Hall, 2 edition, 1971

Kenneth Hoffman and Ray Kunze.Linear Algebra. Prentice-Hall, 2 edition, 1971

work page 1971
[25]

Ignacio Cirac, David Perez-Garcia, Norbert Schuch, and Frank Verstraete

J. Ignacio Cirac, David Perez-Garcia, Norbert Schuch, and Frank Verstraete. Ma- trix product density operators: Renormalization fixed points and boundary theo- ries.Annals of Physics, 378:100–149, 2017

work page 2017
[26]

Springer, 2 edition, 2006

Saugata Basu, Richard Pollack, and Marie-Fran¸ coise Roy.Algorithms in Real Al- gebraic Geometry. Springer, 2 edition, 2006

work page 2006
[27]

A probabilistic logic for verifying continuous-time Markov chains

Ji Guan and Nengkun Yu. A probabilistic logic for verifying continuous-time Markov chains. InTools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the Eu- ropean Joint Conferences on Theory and Practice of Software, ETAPS 2022, Part II, volume 13244 ofLNCS, pages 3–21. Springer, 2022

work page 2022
[28]

Skolem’s prob- lem — on the border between decidability and undecidability

Vesa Halava, Tero Harju, Mika Hirvensalo, and Juhani Karhum¨ aki. Skolem’s prob- lem — on the border between decidability and undecidability. TUCS Technical Report, No 683, April 2005

work page 2005
[29]

Hahn, Andrea Turrini, and Shenggang Ying

Yuan Feng, Ernst M. Hahn, Andrea Turrini, and Shenggang Ying. Model check- ingω-regular properties for quantum Markov chains. InProceedings of the 28th International Conference on Concurrency Theory, CONCUR 2017, volume 85 of LIPIcs, pages 35:1–35:16. Schloss Dagstuhl, 2017

work page 2017
[30]

Lieb, and Hal Tasaki

Ian Affleck, Tom Kennedy, Elliott H. Lieb, and Hal Tasaki. Rigorous results on valence-bond ground states in antiferromagnets.Physical Review Letters, 59(7):799–802, 1987

work page 1987
[31]

Robert Raussendorf and Hans J. Briegel. A one-way quantum computer.Physical Review Letters, 86:5188–5191, 2001

work page 2001
[32]

On the spectral gap of random quantum channels

Carlos E. Gonz´ alez-Guill´ en, Marius Junge, and Ion Nechita. On the spectral gap of random quantum channels.arXiv, abs/1811.08847, 2018. available at https://arxiv.org/abs/1811.08847

work page internal anchor Pith review Pith/arXiv arXiv 2018
[33]

Hastings and Tohru Koma

Matthew B. Hastings and Tohru Koma. Spectral gap and exponential decay of correlations.Communications in Mathematical Physics, 265:781–804, 2006

work page 2006
[34]

The one-dimensional Ising model with a transverse field.Annals of Physics, 57:79–90, 1970

Pierre Pfeuty. The one-dimensional Ising model with a transverse field.Annals of Physics, 57:79–90, 1970

work page 1970
[35]

Oxford University Press, 2003

Thierry Giamarchi.Quantum Physics in One Dimension. Oxford University Press, 2003

work page 2003
[36]

A. Yu. Kitaev. Unpaired majorana fermions in quantum wires.Physics-Uspekhi, 44:131–136, 2001

work page 2001
[37]

Rams, Vid Stojevic, Norbert Schuch, and Frank Ver- straete

Valentin Zauner, Damian Draxler, Laurens Vanderstraeten, Matthias Degroote, Jutho Haegeman, Marek M. Rams, Vid Stojevic, Norbert Schuch, and Frank Ver- straete. Transfer matrices and excitations with matrix product states.New Journal of Physics, 17(5):053002, 2015

work page 2015
[38]

Diagonalizing transfer matrices and matrix product operators: A medley of exact and computational methods.Annual Review of Condensed Matter Physics, 8:355–406, 2017

Jutho Haegeman and Frank Verstraete. Diagonalizing transfer matrices and matrix product operators: A medley of exact and computational methods.Annual Review of Condensed Matter Physics, 8:355–406, 2017. 22

work page 2017
[39]

David Mermin and Herbert Wagner

N. David Mermin and Herbert Wagner. Absence of ferromagnetism or antiferro- magnetism in one-or two-dimensional isotropic Heisenberg models.Physical Review Letters, 17(22):1133–1136, 1966

work page 1966
[40]

Berezinskii

Vadim L. Berezinskii. Destruction of long-range order in one-dimensional and two-dimensional systems possessing a continuous symmetry group. II. quantum systems.Soviet Journal of Experimental and Theoretical Physics, 34:610–616, 1972

work page 1972
[41]

Kosterlitz and David J

John M. Kosterlitz and David J. Thouless. Ordering, metastability and phase transitions in two-dimensional systems.Journal of Physics C: Solid State Physics, 6(7):1181–1203, 1973

work page 1973
[42]

Cambridge University Press, 2 edi- tion, 2011

Subir Sachdev.Quantum Phase Transitions. Cambridge University Press, 2 edi- tion, 2011

work page 2011
[43]

Lieb, and Hal Tasaki

Ian Affleck, Tom Kennedy, Elliott H. Lieb, and Hal Tasaki. Valence bond ground states in isotropic quantum antiferromagnets.Communications in Mathematical Physics, 115(3):477–528, 1988

work page 1988
[44]

On the positivity problem for simple linear recurrence sequences,

Jo¨ el Ouaknine and James Worrell. On the positivity problem for simple linear recurrence sequences,. InAutomata, Languages, and Programming - 41st Interna- tional Colloquium, ICALP 2014, Part II, volume 8573 ofLNCS, pages 318–329. Springer, 2014. 23 A Supplementary Experimental Materials A.1 Details on model preparation We consider two families of models...

work page 2014
[45]

If the sum hits zero periodically, we need the terms of the second largest modulus to determine the sign

By Lemma 2, all terms of the largest modulus are periodic (withN), as well as their sum. If the sum hits zero periodically, we need the terms of the second largest modulus to determine the sign. Otherwise the sign determination is plainly completed. (There is a computable thresholdN 1, after which the sum of all terms of the largest modulus are exponentia...

work page
[46]

(There is a computable thresholdN 2, after which the sum of all terms of the second largest modulus are exponentially dominating the rest.)

At those MPS in which the sum of all terms of the largest modulus hits zero, if the sum of all terms of the second largest modulus is also periodic, the case is reduced to the above; or if the sum is strictly definite, the case is solved. (There is a computable thresholdN 2, after which the sum of all terms of the second largest modulus are exponentially ...

work page
[47]

Otherwise, either the sum crosses zero infinitely often, which is not expo- nentially dominating in the ultimate; or the sum approaches zero arbitrarily close, which is not ensure the computability of the threshold in general, as theeffectiveultimate positivity problem is still open [44]. 27

work page

[1] [1]

Clarke, Orna Grumberg, and Doron A

Edmund M. Clarke, Orna Grumberg, and Doron A. Peled.Model Checking. MIT Press, 1999

work page 1999

[2] [2]

MIT Press, 2008

Christel Baier and Joost-Pieter Katoen.Principles of Model Checking. MIT Press, 2008

work page 2008

[3] [3]

Model-checking quantum systems.National Science Review, 6(1):28–31, 2019

Mingsheng Ying and Yuan Feng. Model-checking quantum systems.National Science Review, 6(1):28–31, 2019

work page 2019

[4] [4]

Cambridge University Press, 2021

Mingsheng Ying and Yuan Feng.Model Checking Quantum Systems: Principles and Algorithms. Cambridge University Press, 2021

work page 2021

[5] [5]

Michael M. Wolf. Quantum channels & operations: Guided tour. Lecture notes available athttps://www-m5.ma.tum.de/foswiki/pub/M5/Allgemeines/ MichaelWolf/QChannelLecture.pdf, 2012

work page 2012

[6] [6]

Daniel A. Lidar. Review of decoherence free subspaces, noiseless subsys- tems, and dynamical decoupling.arXiv, abs/1208.5791, 2012. available at https://arxiv.org/abs/1208.5791

work page internal anchor Pith review Pith/arXiv arXiv 2012

[7] [7]

The Structure of Decoherence-free Subsystems

Ji Guan, Yuan Feng, and Mingsheng Ying. The structure of decoherence-free subsystems.arXiv, abs/1802.04904, 2018. available at https://arxiv.org/abs/1802.04904

work page internal anchor Pith review Pith/arXiv arXiv 2018

[8] [8]

Morgan Kaufmann, 2 edition, 2024

Mingsheng Ying.Foundations of Quantum Programming. Morgan Kaufmann, 2 edition, 2024

work page 2024

[9] [9]

Springer, 2019

Bei Zeng, Xie Chen, Duan-Lu Zhou, and Xiao-Gang Wen.Quantum Information Meets Quantum Matter: From Quantum Entanglement to Topological Phase of Many-Body Systems. Springer, 2019

work page 2019

[10] [10]

Regular language quantum states

Marta Florido-Llin` as, ´Alvaro M. Alhambra, David P´ erez-Garc´ ıa, and J. Ignacio Cirac. Regular language quantum states.arXiv, abs/2407.17641, 2024. available at https://arxiv.org/abs/2407.17641

work page internal anchor Pith review Pith/arXiv arXiv 2024

[11] [11]

The density-matrix renormalization group in the age of matrix product states.Annals of Physics, 326(1):96–192, 2011

Ulrich Schollw¨ ock. The density-matrix renormalization group in the age of matrix product states.Annals of Physics, 326(1):96–192, 2011

work page 2011

[12] [12]

Hastings

Matthew B. Hastings. An area law for one-dimensional quantum systems.Journal of Statistical Mechanics: Theory and Experiment, 2007(08):P08024, 2007

work page 2007

[13] [13]

Vazirani

Dorit Aharonov, Itai Arad, Zeph Landau, and Umesh V. Vazirani. The 1d area law and the complexity of quantum states: A combinatorial approach. InIEEE 52nd Annual Symposium on Foundations of Computer Science, FOCS 2011, pages 324–333. IEEE Computer Society, 2011

work page 2011

[14] [14]

Clarke, E

Edmund M. Clarke, E. Allen Emerson, and A. Prasad Sistla. Automatic verifica- tion of finite-state concurrent systems using temporal logic specifications.ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986

work page 1986

[15] [15]

Model checking quantum Markov chains.Journal of Computer and System Sciences, 79(7):1181–1198, 2013

Yuan Feng, Nengkun Yu, and Mingsheng Ying. Model checking quantum Markov chains.Journal of Computer and System Sciences, 79(7):1181–1198, 2013

work page 2013

[16] [16]

Model Checking Quantum Systems --- A Survey

Mingsheng Ying and Yuan Feng. Model checking quantum systems — A survey. arXiv, abs/1807.09466, 2018. available at https://arxiv.org/abs/1807.09466

work page internal anchor Pith review Pith/arXiv arXiv 2018

[17] [17]

A practical introduction to tensor networks: Matrix product states and projected entangled pair states.Annals of Physics, 349:117–158, 2014

Rom´ an Or´ us. A practical introduction to tensor networks: Matrix product states and projected entangled pair states.Annals of Physics, 349:117–158, 2014

work page 2014

[18] [18]

Wolf, and J

David P´ erez-Garc´ ıa, Frank Verstraete, Michael M. Wolf, and J. Ignacio Cirac. Matrix product state representations.Quantum Information & Computation, 7(5):401–430, 2007

work page 2007

[19] [19]

Mark Fannes, Bruno Nachtergaele, and Reinhard F. Werner. Finitely corre- lated states on quantum spin chains.Communications in Mathematical Physics, 144(3):443–490, 1992. 21

work page 1992

[20] [20]

Nielsen and Isaac L

Michael A. Nielsen and Isaac L. Chuang.Quantum Computation and Quantum Information. Cambridge University Press, 2000

work page 2000

[21] [21]

Ignacio Cirac, David Perez-Garcia, Norbert Schuch, and Frank Verstraete

J. Ignacio Cirac, David Perez-Garcia, Norbert Schuch, and Frank Verstraete. Ma- trix product states and projected entangled pair states: Concepts, symmetries, theorems.Reviews of Modern Physics, 93(4):045003, 2021

work page 2021

[22] [22]

Ignacio Cirac, Norbert Schuch, and David Perez-Garcia

Gemma De las Cuevas, J. Ignacio Cirac, Norbert Schuch, and David Perez-Garcia. Irreducible forms of matrix product states: Theory and applications.Journal of Mathematical Physics, 58(12):121901, 2017

work page 2017

[23] [23]

Completely positive linear maps on complex matrices.Linear Algebra and Its Applications, 10(3):285–290, 1975

Man-Duen Choi. Completely positive linear maps on complex matrices.Linear Algebra and Its Applications, 10(3):285–290, 1975

work page 1975

[24] [24]

Prentice-Hall, 2 edition, 1971

Kenneth Hoffman and Ray Kunze.Linear Algebra. Prentice-Hall, 2 edition, 1971

work page 1971

[25] [25]

Ignacio Cirac, David Perez-Garcia, Norbert Schuch, and Frank Verstraete

J. Ignacio Cirac, David Perez-Garcia, Norbert Schuch, and Frank Verstraete. Ma- trix product density operators: Renormalization fixed points and boundary theo- ries.Annals of Physics, 378:100–149, 2017

work page 2017

[26] [26]

Springer, 2 edition, 2006

Saugata Basu, Richard Pollack, and Marie-Fran¸ coise Roy.Algorithms in Real Al- gebraic Geometry. Springer, 2 edition, 2006

work page 2006

[27] [27]

A probabilistic logic for verifying continuous-time Markov chains

Ji Guan and Nengkun Yu. A probabilistic logic for verifying continuous-time Markov chains. InTools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the Eu- ropean Joint Conferences on Theory and Practice of Software, ETAPS 2022, Part II, volume 13244 ofLNCS, pages 3–21. Springer, 2022

work page 2022

[28] [28]

Skolem’s prob- lem — on the border between decidability and undecidability

Vesa Halava, Tero Harju, Mika Hirvensalo, and Juhani Karhum¨ aki. Skolem’s prob- lem — on the border between decidability and undecidability. TUCS Technical Report, No 683, April 2005

work page 2005

[29] [29]

Hahn, Andrea Turrini, and Shenggang Ying

Yuan Feng, Ernst M. Hahn, Andrea Turrini, and Shenggang Ying. Model check- ingω-regular properties for quantum Markov chains. InProceedings of the 28th International Conference on Concurrency Theory, CONCUR 2017, volume 85 of LIPIcs, pages 35:1–35:16. Schloss Dagstuhl, 2017

work page 2017

[30] [30]

Lieb, and Hal Tasaki

Ian Affleck, Tom Kennedy, Elliott H. Lieb, and Hal Tasaki. Rigorous results on valence-bond ground states in antiferromagnets.Physical Review Letters, 59(7):799–802, 1987

work page 1987

[31] [31]

Robert Raussendorf and Hans J. Briegel. A one-way quantum computer.Physical Review Letters, 86:5188–5191, 2001

work page 2001

[32] [32]

On the spectral gap of random quantum channels

Carlos E. Gonz´ alez-Guill´ en, Marius Junge, and Ion Nechita. On the spectral gap of random quantum channels.arXiv, abs/1811.08847, 2018. available at https://arxiv.org/abs/1811.08847

work page internal anchor Pith review Pith/arXiv arXiv 2018

[33] [33]

Hastings and Tohru Koma

Matthew B. Hastings and Tohru Koma. Spectral gap and exponential decay of correlations.Communications in Mathematical Physics, 265:781–804, 2006

work page 2006

[34] [34]

The one-dimensional Ising model with a transverse field.Annals of Physics, 57:79–90, 1970

Pierre Pfeuty. The one-dimensional Ising model with a transverse field.Annals of Physics, 57:79–90, 1970

work page 1970

[35] [35]

Oxford University Press, 2003

Thierry Giamarchi.Quantum Physics in One Dimension. Oxford University Press, 2003

work page 2003

[36] [36]

A. Yu. Kitaev. Unpaired majorana fermions in quantum wires.Physics-Uspekhi, 44:131–136, 2001

work page 2001

[37] [37]

Rams, Vid Stojevic, Norbert Schuch, and Frank Ver- straete

Valentin Zauner, Damian Draxler, Laurens Vanderstraeten, Matthias Degroote, Jutho Haegeman, Marek M. Rams, Vid Stojevic, Norbert Schuch, and Frank Ver- straete. Transfer matrices and excitations with matrix product states.New Journal of Physics, 17(5):053002, 2015

work page 2015

[38] [38]

Diagonalizing transfer matrices and matrix product operators: A medley of exact and computational methods.Annual Review of Condensed Matter Physics, 8:355–406, 2017

Jutho Haegeman and Frank Verstraete. Diagonalizing transfer matrices and matrix product operators: A medley of exact and computational methods.Annual Review of Condensed Matter Physics, 8:355–406, 2017. 22

work page 2017

[39] [39]

David Mermin and Herbert Wagner

N. David Mermin and Herbert Wagner. Absence of ferromagnetism or antiferro- magnetism in one-or two-dimensional isotropic Heisenberg models.Physical Review Letters, 17(22):1133–1136, 1966

work page 1966

[40] [40]

Berezinskii

Vadim L. Berezinskii. Destruction of long-range order in one-dimensional and two-dimensional systems possessing a continuous symmetry group. II. quantum systems.Soviet Journal of Experimental and Theoretical Physics, 34:610–616, 1972

work page 1972

[41] [41]

Kosterlitz and David J

John M. Kosterlitz and David J. Thouless. Ordering, metastability and phase transitions in two-dimensional systems.Journal of Physics C: Solid State Physics, 6(7):1181–1203, 1973

work page 1973

[42] [42]

Cambridge University Press, 2 edi- tion, 2011

Subir Sachdev.Quantum Phase Transitions. Cambridge University Press, 2 edi- tion, 2011

work page 2011

[43] [43]

Lieb, and Hal Tasaki

Ian Affleck, Tom Kennedy, Elliott H. Lieb, and Hal Tasaki. Valence bond ground states in isotropic quantum antiferromagnets.Communications in Mathematical Physics, 115(3):477–528, 1988

work page 1988

[44] [44]

On the positivity problem for simple linear recurrence sequences,

Jo¨ el Ouaknine and James Worrell. On the positivity problem for simple linear recurrence sequences,. InAutomata, Languages, and Programming - 41st Interna- tional Colloquium, ICALP 2014, Part II, volume 8573 ofLNCS, pages 318–329. Springer, 2014. 23 A Supplementary Experimental Materials A.1 Details on model preparation We consider two families of models...

work page 2014

[45] [45]

If the sum hits zero periodically, we need the terms of the second largest modulus to determine the sign

By Lemma 2, all terms of the largest modulus are periodic (withN), as well as their sum. If the sum hits zero periodically, we need the terms of the second largest modulus to determine the sign. Otherwise the sign determination is plainly completed. (There is a computable thresholdN 1, after which the sum of all terms of the largest modulus are exponentia...

work page

[46] [46]

(There is a computable thresholdN 2, after which the sum of all terms of the second largest modulus are exponentially dominating the rest.)

At those MPS in which the sum of all terms of the largest modulus hits zero, if the sum of all terms of the second largest modulus is also periodic, the case is reduced to the above; or if the sum is strictly definite, the case is solved. (There is a computable thresholdN 2, after which the sum of all terms of the second largest modulus are exponentially ...

work page

[47] [47]

Otherwise, either the sum crosses zero infinitely often, which is not expo- nentially dominating in the ultimate; or the sum approaches zero arbitrarily close, which is not ensure the computability of the threshold in general, as theeffectiveultimate positivity problem is still open [44]. 27

work page