Computational Complexity of Model-Checking Quantum Pushdown Systems

Deren Lin; Tianrong Lin

arxiv: 2506.18439 · v14 · submitted 2025-06-23 · 💻 cs.LO · cs.CC

Computational Complexity of Model-Checking Quantum Pushdown Systems

Deren Lin , Tianrong Lin This is my paper

Pith reviewed 2026-05-19 08:12 UTC · model grok-4.3

classification 💻 cs.LO cs.CC

keywords quantum pushdown systemsmodel checkingundecidabilityPCTLquantum Markov chainsbounded PCTLPost Correspondence Problemcomputational complexity

0 comments

The pith

Model-checking stateless quantum pushdown systems against PCTL is undecidable.

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

The paper extends classical probabilistic pushdown systems to quantum versions called qPDS and associated quantum Markov chains. It gives a necessary and sufficient condition for a qPDS to be well-formed and shows how to extend its local transitions into a unitary operator. The main result establishes that model-checking stateless quantum pushdown systems (qBPA) against probabilistic computational tree logic (PCTL) admits no algorithm in general. For the restricted bounded fragment bPCTL the same problem becomes decidable yet NP-hard, via a direct reduction from the bounded Post Correspondence Problem.

Core claim

Stateless quantum pushdown systems (qBPA) admit no general algorithm for model-checking against probabilistic computational tree logic (PCTL), because the decision problem is undecidable. The result is obtained by first defining well-formed qPDS whose transitions extend to unitary operators, then reducing the verification question to properties of the induced quantum Markov chain.

What carries the argument

Stateless quantum pushdown automaton (qBPA), defined as a quantum extension of a probabilistic pushdown system whose local transitions extend to a unitary time-evolution operator on the quantum state space.

If this is right

No algorithm exists that decides, for arbitrary qBPA and PCTL formulas, whether the quantum system satisfies the formula.
Model-checking qBPA against the bounded fragment bPCTL is decidable.
The decidable bPCTL case is NP-hard, established by polynomial reduction from the bounded Post Correspondence Problem.

Where Pith is reading between the lines

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

Verification procedures for quantum protocols with unbounded stack memory will inherit undecidability barriers already known for classical infinite-state systems.
Restricting attention to bounded temporal operators may yield practical semi-decision methods even when full PCTL remains intractable.
The same reduction technique could be reused to prove complexity results for other quantum automata models that combine finite control with an infinite quantum memory.

Load-bearing premise

A well-formed quantum pushdown system admits an extension of its local transition function to a unitary operator that keeps the overall evolution physically consistent.

What would settle it

An explicit decision procedure that, for every stateless qPDS and every PCTL formula, returns whether the system satisfies the formula and always terminates.

read the original abstract

In this paper, we study the problem of model-checking quantum pushdown systems from a computational complexity point of view. We arrive at the following equally important, interesting new results: We first extend the notions of the {\it probabilistic pushdown systems} and {\it Markov chains} to their quantum counterparts, i.e., {\em quantum pushdown system (qPDS)} and {\em quantum Markov chains}, and prove a necessary and sufficient condition for a qPDS to be well formed, also presenting a method to extend the local transition function of a well-formed qPDS to a unitary local time evolution operator. Next, we investigate the question of whether it is necessary to define a quantum analogue of {\it probabilistic computational tree logic} to describe the probabilistic and branching-time properties of the {\it quantum Markov chain}. We study its model-checking question and show that model-checking of {\it stateless quantum pushdown systems (qBPA)} against {\it probabilistic computational tree logic (PCTL)} is generally undecidable, i.e., there exists no algorithm for model-checking {\it stateless quantum pushdown systems (qBPA)} against {\it probabilistic computational tree logic}. We then study in which case there exists an algorithm for model-checking {\it stateless quantum pushdown systems} and show that the problem of model-checking {\it stateless quantum pushdown systems (qBPA)} against {\it bounded probabilistic computational tree logic} (bPCTL) is decidable, and further show that this problem is in $\mathit{NP}$-hard. Our reduction is from the {\it bounded Post Correspondence Problem} for the first time, a well-known $\mathit{NP}$-complete problem.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper establishes undecidability of PCTL model-checking for stateless quantum pushdown systems and NP-hardness for the bounded case via bounded PCP, but the reduction needs checking against the well-formedness condition.

read the letter

The main takeaway is that model-checking stateless quantum pushdown systems against PCTL is undecidable while the bounded version sits in NP-hard. The authors first define quantum pushdown systems and quantum Markov chains as direct extensions of the probabilistic versions. They prove a necessary and sufficient condition for well-formedness and give an explicit way to lift the local transition function to a unitary operator. That groundwork lets them move to the complexity results. The undecidability claim for full PCTL on qBPA follows from a reduction, and the NP-hardness for bPCTL comes from a reduction from bounded Post Correspondence Problem, which they note is new in this setting. Both results are presented cleanly in the abstract and appear to be the core contribution. The work is technically grounded in standard techniques from automata theory and complexity, applied to the quantum case. The well-formedness condition and unitary extension method are useful additions on their own because they make the model precise before the hardness arguments begin. One soft spot worth checking is whether every system constructed in the undecidability reduction actually satisfies the well-formedness criterion. If the local transition amplitudes chosen for the reduction fail the operator-sum or orthogonality requirements, those instances would sit outside the class where the unitary time evolution is defined and the quantum Markov-chain semantics hold. The abstract places the well-formedness proof before the complexity claims, which suggests the authors are aware of the issue, but the reduction details will show whether it is handled. This paper is aimed at researchers working on quantum automata, verification of quantum systems with memory, and complexity of branching-time logics. A reader already familiar with probabilistic pushdown systems and PCTL will see the extension and the new hardness proof without much extra background. It deserves a serious referee because the claims are concrete, the approach is standard but freshly applied, and the results would matter to the small community that cares about quantum model checking. I would send it out for review with a request that the referees pay close attention to the reduction constructions and how they interact with the well-formedness condition.

Referee Report

1 major / 1 minor

Summary. The manuscript extends probabilistic pushdown systems to quantum pushdown systems (qPDS) and quantum Markov chains. It proves a necessary and sufficient condition for a qPDS to be well-formed and gives an explicit method to extend the local transition function to a unitary local time evolution operator. It then shows that model-checking stateless qPDS (qBPA) against PCTL is undecidable in general, while model-checking against bounded PCTL (bPCTL) is decidable and NP-hard via a reduction from the bounded Post Correspondence Problem.

Significance. If the central claims hold, the work supplies foundational definitions and complexity bounds for verification of quantum systems with stack-based memory. The well-formedness criterion and unitary-extension construction are useful for ensuring physical consistency. The undecidability result marks a clear limit for PCTL-style properties, and the NP-hardness result for bPCTL (via bounded PCP) supplies a concrete lower bound that had not previously been shown in this setting.

major comments (1)

[proof of undecidability for qBPA vs. PCTL] The undecidability proof for qBPA model-checking against PCTL relies on a reduction that must produce only well-formed qBPAs. The manuscript should explicitly confirm that every constructed instance satisfies the necessary and sufficient well-formedness condition (the operator-sum and orthogonality requirements on the local transitions) so that the unitary extension is defined and the quantum Markov-chain semantics apply. If this verification is absent or incomplete, the reduction does not establish undecidability inside the intended model class.

minor comments (1)

The abstract states that the bPCTL reduction is 'for the first time' from bounded PCP; a brief comparison with prior reductions for related quantum or probabilistic models would help readers assess novelty.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the detailed review and for highlighting the need to ensure the reduction instances remain within the well-formed qBPA class. We address the single major comment below and will incorporate the requested clarification in the revised manuscript.

read point-by-point responses

Referee: [proof of undecidability for qBPA vs. PCTL] The undecidability proof for qBPA model-checking against PCTL relies on a reduction that must produce only well-formed qBPAs. The manuscript should explicitly confirm that every constructed instance satisfies the necessary and sufficient well-formedness condition (the operator-sum and orthogonality requirements on the local transitions) so that the unitary extension is defined and the quantum Markov-chain semantics apply. If this verification is absent or incomplete, the reduction does not establish undecidability inside the intended model class.

Authors: We agree that explicit verification is necessary for the reduction to be fully rigorous. In the current proof of undecidability (Theorem 4.1), the constructed qBPAs are obtained by a direct quantum lifting of the classical BPA instances used in the PCTL undecidability proof; each local transition is defined so that the Kraus operators sum to the identity on the relevant subspace and the orthogonality condition holds by construction (the supports of distinct control states remain orthogonal). Nevertheless, we did not include a separate lemma stating this fact for the reduction family. We will add a short lemma (or a dedicated paragraph immediately after the reduction definition) that invokes the necessary-and-sufficient well-formedness criterion proved in Section 3 and verifies that every instance satisfies both the operator-sum and orthogonality requirements. This will make the applicability of the unitary extension and the quantum Markov-chain semantics fully explicit. revision: yes

Circularity Check

0 steps flagged

No circularity: results rest on external reductions and an independently proven well-formedness condition

full rationale

The paper first derives a necessary and sufficient condition for a qPDS to be well-formed together with an explicit extension of the local transition function to a unitary operator; this step is self-contained and does not presuppose the later complexity results. Undecidability of qBPA model-checking against PCTL is obtained by reduction from a standard undecidable problem outside the paper, while NP-hardness of the bounded-PCTL case is obtained by a fresh reduction from the known NP-complete bounded Post Correspondence Problem. No equation or definition is shown to be equivalent to its own input by construction, no fitted parameter is relabeled as a prediction, and no load-bearing premise collapses to a self-citation. The derivation chain therefore remains independent of the target claims.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 2 invented entities

The central claims rest on new definitions of qPDS and quantum Markov chains plus standard quantum mechanics requirements for unitarity; no free parameters are introduced and the invented entities are the quantum extensions themselves.

axioms (1)

domain assumption Quantum state evolution must be described by unitary operators to preserve norms and probabilities
Invoked when extending the local transition function of a well-formed qPDS to a unitary local time evolution operator.

invented entities (2)

quantum pushdown system (qPDS) no independent evidence
purpose: Quantum analogue of probabilistic pushdown systems for modeling stack-based quantum computation
Newly defined in the paper as the core object of study.
quantum Markov chain no independent evidence
purpose: Quantum counterpart to classical Markov chains for describing state transitions
Introduced to support the model-checking analysis.

pith-pipeline@v0.9.0 · 5836 in / 1519 out tokens · 48954 ms · 2026-05-19T08:12:47.201890+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

22 extracted references · 22 canonical work pages

[1]

Hunting for bugs in code coverage tools via randomized differential testing

[A1] Anonymous authors. Chernoff bound. Avaliable at https://en.wikipedia.org/wiki/Chernoff bound. [AGS19] Scott Aaronson, Daniel Grier and Luke Schaeffer. A Quantum Query Complexity Trichotomy for Regular Languages. In: IEEE 60th An- nual Symposium on Foundations of Computer Science, 2019, pp. 942–965. https://doi.org/10.1109/FOCS.2019.00061. [AB09] Sanj...

work page doi:10.1109/focs.2019.00061 2019
[2]

[Acc76] L. Accardi. Nonrelativistic quantum mechanics as a noncommutative Markov process. Advances in Mathematics 20, 329 – 366 (1976). [BV97] E. Bernstein and U. Vazirani. Quantum Complexity Theory . SIAM Journal on Computing, Vol. 26, No. 5, pp. 1411–1473, October

work page 1976
[3]

[BK08] C

https://doi.org/10.1137/S0097539796300921. [BK08] C. Baier and J. P. Katoen. Principles of Model Checking. MIT Press,

work page doi:10.1137/s0097539796300921
[4]

Br´ azdil, V

42 [BBFK14] T. Br´ azdil, V. Broˇ zek, V. Forejt and A. Kuˇ cera. Branching- time model-checking of probabilistic pushdown automata . Jour- nal of Computer and System Sciences 80 (2014) 139 –

work page 2014
[5]

[BCM08] P

https://doi.org/10.1016/j.jcss.2013.07.001. [BCM08] P. Baltazar, R. Chadha and P. Mateus. Quantum computation tree logic — model checking and complete calculus . International Journal of Quantum Information, Vol. 6, No. 2 (2008) 219 –

work page doi:10.1016/j.jcss.2013.07.001 2013
[6]

[CGP99] E

https://doi.org/10.1142/S0219749908003530. [CGP99] E. M. Clarke, O. Grumberg and D. A. Peled. Model Checking. MIT Press,

work page doi:10.1142/s0219749908003530
[7]

[Coo71] Stephen A. Cook. The complexity of theorem-proving proce- dures. In: Proceedings of the Third Annual ACM Sym- posium on Theory of Computing, May 1971, Pages 151–158. https://doi.org/10.1145/800157.805047. [Deu85] D. Deutsch. Quantum theory, the Church–Turing principle and the universal quantum computer . Proceedings of The Royal Society of London....

work page doi:10.1145/800157.805047 1971
[8]

Esparza, A

[EKM06] J. Esparza, A. Kuˇ cera and R. Mayr, Model-checking probabilistic pushdown automata . Logical Methods in Computer Science, Vol. 2 (1:2) 2006, pp. 1 –

work page 2006
[9]

[EKS03] J

https://doi.org/10.2168/LMCS-2(1:2)2006. [EKS03] J. Esparza, A. Kuˇ cera and S. Schwoon, Model checking LTL with regular valuations for pushdown systems . Information and Com- putation 186, 2003, pp. 355 –

work page doi:10.2168/lmcs-2(1:2)2006 2006
[10]

[For03] Lance Fortnow

https://doi.org/10.1016/S0890- 5401(03)00139-1. [For03] Lance Fortnow. One complexity theorist’s view of quantum computing. Theoretical Computer Science 292 (2003) 597–610. https://doi.org/10.1016/S0304-3975(01)00377-2. 43 [Gud08] S. Gudder. Quantum Markov chains . Journal of Mathematical Physics 49, 072105 (2008); https://doi.org/10.1063/1.2953952. [GJ79...

work page doi:10.1016/s0890- 2003
[11]

Hansson and B

[HJ94] H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing 6 (1994) 512 –

work page 1994
[12]

[Hir04] Mika Hirvensalo

https://doi.org/10.1007/BF01211866. [Hir04] Mika Hirvensalo. Quantum Computing. Second ed., Springer, Berlin,

work page doi:10.1007/bf01211866
[13]

Knodacs and J

[KW97] A. Knodacs and J. Watrous. On the power of quantum fi- nite state automata . In: Proceedings 38th Annual Sympo- sium on Foundations of Computer Science, 1997, pp. 66 –

work page 1997
[14]

[KNP07] Marta Kwiatkowska, Gethin Norman, and David Parker

https://doi.org/10.1109/SFCS.1997.646094. [KNP07] Marta Kwiatkowska, Gethin Norman, and David Parker. Stochastic Model Checking. In: Formal Methods for Performance Evaluation. SFM

work page doi:10.1109/sfcs.1997.646094 1997
[15]

Springer, Berlin, Heidelberg. pp. 220–270. https://doi.org/10.1007/978-3-540- 72522-0

work page doi:10.1007/978-3-540-
[16]

Model-Checking PCTL Properties of Stateless Probabilistic Pushdown Systems

[LL24] Deren Lin and Tianrong Lin. Model-Checking PCTL Properties of Stateless Probabilistic Pushdown Systems. arXiv: 1405.4806,

work page arXiv
[17]

Model-Checking PCTL Properties of Stateless Probabilistic Pushdown Systems

https://doi.org/10.48550/arXiv.1405.4806. 44 [Lin12] Tianrong Lin. Another approach to the equivalence of measure- many one-way quantum finite automata and its application. Journal of Computer and System Sciences 78 (2012) 807–821. https://doi.org/10.1016/j.jcss.2012.01.004. [MC00] C. Moore and J. P. Crutchfield. Quantum automata and quantum grammars. The...

work page doi:10.48550/arxiv.1405.4806 2012
[18]

[NC00] M

https://doi.org/10.1016/S0304-3975(98)00191-1. [NC00] M. A. Nielsen and I. L. Chuang. Quantum computation and quantum information. Cambridge University Press, Cambridge,

work page doi:10.1016/s0304-3975(98)00191-1
[19]

[Pos46] E. L. Post. A variant of a recursively unsolvable problem . Bulletin of the American Mathematical Society 52, 1946, pp. 264 –

work page 1946
[20]

[Rab63] M. O. Rabin. Probabilistic automata. Information and Control 6 (1963) 230–244. https://doi.org/10.1016/S0019-9958(63)90290-0. [Sho97] Peter W. Shor. Polynomial-time algorithms for prime factoriza- tion and discrete logarithms on a quantum computer. SIAM Jour- nal on Computing, vol. 26, No. 5, pp. 1484–1509, October

work page doi:10.1016/s0019-9958(63)90290-0 1963
[21]

SIAM Journal on Computing 26(5), 1484– 1509 (Oct 1997)

https://doi.org/10.1137/S0097539795293172. [Shi95] A. N. Shiryaev. Probability, ( 2nd Edition). Springer-Verlag, New York,

work page doi:10.1137/s0097539795293172
[22]

Quantum circuit complexity

[Yao93] Andrew Chi-Chih Yao. Quantum circuit complexity. In: Proceedings of IEEE 34th Annual Foundations of Computer Science, 1993, pp. 352–361. https://doi.org/10.1109/SFCS.1993.366852. 45

work page doi:10.1109/sfcs.1993.366852 1993

[1] [1]

Hunting for bugs in code coverage tools via randomized differential testing

[A1] Anonymous authors. Chernoff bound. Avaliable at https://en.wikipedia.org/wiki/Chernoff bound. [AGS19] Scott Aaronson, Daniel Grier and Luke Schaeffer. A Quantum Query Complexity Trichotomy for Regular Languages. In: IEEE 60th An- nual Symposium on Foundations of Computer Science, 2019, pp. 942–965. https://doi.org/10.1109/FOCS.2019.00061. [AB09] Sanj...

work page doi:10.1109/focs.2019.00061 2019

[2] [2]

[Acc76] L. Accardi. Nonrelativistic quantum mechanics as a noncommutative Markov process. Advances in Mathematics 20, 329 – 366 (1976). [BV97] E. Bernstein and U. Vazirani. Quantum Complexity Theory . SIAM Journal on Computing, Vol. 26, No. 5, pp. 1411–1473, October

work page 1976

[3] [3]

[BK08] C

https://doi.org/10.1137/S0097539796300921. [BK08] C. Baier and J. P. Katoen. Principles of Model Checking. MIT Press,

work page doi:10.1137/s0097539796300921

[4] [4]

Br´ azdil, V

42 [BBFK14] T. Br´ azdil, V. Broˇ zek, V. Forejt and A. Kuˇ cera. Branching- time model-checking of probabilistic pushdown automata . Jour- nal of Computer and System Sciences 80 (2014) 139 –

work page 2014

[5] [5]

[BCM08] P

https://doi.org/10.1016/j.jcss.2013.07.001. [BCM08] P. Baltazar, R. Chadha and P. Mateus. Quantum computation tree logic — model checking and complete calculus . International Journal of Quantum Information, Vol. 6, No. 2 (2008) 219 –

work page doi:10.1016/j.jcss.2013.07.001 2013

[6] [6]

[CGP99] E

https://doi.org/10.1142/S0219749908003530. [CGP99] E. M. Clarke, O. Grumberg and D. A. Peled. Model Checking. MIT Press,

work page doi:10.1142/s0219749908003530

[7] [7]

[Coo71] Stephen A. Cook. The complexity of theorem-proving proce- dures. In: Proceedings of the Third Annual ACM Sym- posium on Theory of Computing, May 1971, Pages 151–158. https://doi.org/10.1145/800157.805047. [Deu85] D. Deutsch. Quantum theory, the Church–Turing principle and the universal quantum computer . Proceedings of The Royal Society of London....

work page doi:10.1145/800157.805047 1971

[8] [8]

Esparza, A

[EKM06] J. Esparza, A. Kuˇ cera and R. Mayr, Model-checking probabilistic pushdown automata . Logical Methods in Computer Science, Vol. 2 (1:2) 2006, pp. 1 –

work page 2006

[9] [9]

[EKS03] J

https://doi.org/10.2168/LMCS-2(1:2)2006. [EKS03] J. Esparza, A. Kuˇ cera and S. Schwoon, Model checking LTL with regular valuations for pushdown systems . Information and Com- putation 186, 2003, pp. 355 –

work page doi:10.2168/lmcs-2(1:2)2006 2006

[10] [10]

[For03] Lance Fortnow

https://doi.org/10.1016/S0890- 5401(03)00139-1. [For03] Lance Fortnow. One complexity theorist’s view of quantum computing. Theoretical Computer Science 292 (2003) 597–610. https://doi.org/10.1016/S0304-3975(01)00377-2. 43 [Gud08] S. Gudder. Quantum Markov chains . Journal of Mathematical Physics 49, 072105 (2008); https://doi.org/10.1063/1.2953952. [GJ79...

work page doi:10.1016/s0890- 2003

[11] [11]

Hansson and B

[HJ94] H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing 6 (1994) 512 –

work page 1994

[12] [12]

[Hir04] Mika Hirvensalo

https://doi.org/10.1007/BF01211866. [Hir04] Mika Hirvensalo. Quantum Computing. Second ed., Springer, Berlin,

work page doi:10.1007/bf01211866

[13] [13]

Knodacs and J

[KW97] A. Knodacs and J. Watrous. On the power of quantum fi- nite state automata . In: Proceedings 38th Annual Sympo- sium on Foundations of Computer Science, 1997, pp. 66 –

work page 1997

[14] [14]

[KNP07] Marta Kwiatkowska, Gethin Norman, and David Parker

https://doi.org/10.1109/SFCS.1997.646094. [KNP07] Marta Kwiatkowska, Gethin Norman, and David Parker. Stochastic Model Checking. In: Formal Methods for Performance Evaluation. SFM

work page doi:10.1109/sfcs.1997.646094 1997

[15] [15]

Springer, Berlin, Heidelberg. pp. 220–270. https://doi.org/10.1007/978-3-540- 72522-0

work page doi:10.1007/978-3-540-

[16] [16]

Model-Checking PCTL Properties of Stateless Probabilistic Pushdown Systems

[LL24] Deren Lin and Tianrong Lin. Model-Checking PCTL Properties of Stateless Probabilistic Pushdown Systems. arXiv: 1405.4806,

work page arXiv

[17] [17]

Model-Checking PCTL Properties of Stateless Probabilistic Pushdown Systems

https://doi.org/10.48550/arXiv.1405.4806. 44 [Lin12] Tianrong Lin. Another approach to the equivalence of measure- many one-way quantum finite automata and its application. Journal of Computer and System Sciences 78 (2012) 807–821. https://doi.org/10.1016/j.jcss.2012.01.004. [MC00] C. Moore and J. P. Crutchfield. Quantum automata and quantum grammars. The...

work page doi:10.48550/arxiv.1405.4806 2012

[18] [18]

[NC00] M

https://doi.org/10.1016/S0304-3975(98)00191-1. [NC00] M. A. Nielsen and I. L. Chuang. Quantum computation and quantum information. Cambridge University Press, Cambridge,

work page doi:10.1016/s0304-3975(98)00191-1

[19] [19]

[Pos46] E. L. Post. A variant of a recursively unsolvable problem . Bulletin of the American Mathematical Society 52, 1946, pp. 264 –

work page 1946

[20] [20]

[Rab63] M. O. Rabin. Probabilistic automata. Information and Control 6 (1963) 230–244. https://doi.org/10.1016/S0019-9958(63)90290-0. [Sho97] Peter W. Shor. Polynomial-time algorithms for prime factoriza- tion and discrete logarithms on a quantum computer. SIAM Jour- nal on Computing, vol. 26, No. 5, pp. 1484–1509, October

work page doi:10.1016/s0019-9958(63)90290-0 1963

[21] [21]

SIAM Journal on Computing 26(5), 1484– 1509 (Oct 1997)

https://doi.org/10.1137/S0097539795293172. [Shi95] A. N. Shiryaev. Probability, ( 2nd Edition). Springer-Verlag, New York,

work page doi:10.1137/s0097539795293172

[22] [22]

Quantum circuit complexity

[Yao93] Andrew Chi-Chih Yao. Quantum circuit complexity. In: Proceedings of IEEE 34th Annual Foundations of Computer Science, 1993, pp. 352–361. https://doi.org/10.1109/SFCS.1993.366852. 45

work page doi:10.1109/sfcs.1993.366852 1993