Source-linked AI summary
The Emptiness Problem for Quantum Finite Automata with Classical States
Jyun-Ao Lin, Patrick Totzke, Yun Chen Tsai, Di-De Yen
TL;DR
The paper asks how QFACs compare expressively and whether their recognized languages are empty under cut-point semantics. It reduces emptiness to QFA–finite-automaton intersection, relates flat cases to the higher-dimensional orbit problem, and develops a witness search procedure for one-loop QFACs. It proves that strict-threshold emptiness is decidable while non-strict-threshold emptiness is undecidable, and gives a sound, uniformly semi-complete strict-case procedure for one-loop witnesses.
Problem
The paper studies QFAC expressiveness and asks whether a QFAC recognizes any word for a specified threshold and comparison operator.
Method
The paper reduces QFAC emptiness to QFA–finite-automaton intersection, relates one-loop flat cases to the higher-dimensional orbit problem, and generates witnesses with nonlinear integer programming.
Results
QFAC emptiness is decidable for strict thresholds and undecidable for non-strict thresholds; the one-loop witness procedure is sound and semi-complete for strict thresholds.
Takeaways & Limitations
QFACs strictly extend regular-language and QFA expressiveness, while one-loop witness search supports verification of examples including Grover’s search and quantum random walks.
Takeaways & Limitations
The decidability status remains unclear for flat QFACs, including specifically one-loop QFACs, beyond the reduction to the higher-dimensional orbit problem.
Abstract
from arXiv · showhide
Quantum Finite Automata with Classical states (QFACs) are nondeterministic finite automata over a finite alphabet of quantum operations. We study expressiveness of this model on finite words and the corresponding emptiness problem. We show that regular languages are incomparable with those definable by Quantum Finite Automata (QFAs) and that both are strictly subsumed by QFAC-definable languages. We show that the emptiness problem for a QFAC can be reduced to the emptiness of the language intersection of a QFA and a finite automaton. This intersection is known to be decidable for strict thresholds but undecidable for non-strict cases. Furthermore, we consider the problem for flat QFACs, a restriction where the underlying automata contain no nested loops, and relate it to the higher-dimensional orbit problem, a long-standing open challenge in dynamical systems. Finally, we propose a sound and semi-complete witness searching procedure to verify the non-emptiness of one-loop QFACs, which are sufficiently expressive to represent some prominent quantum algorithms, such as Grover's search and quantum random walks.
1 Introduction
The paper motivates QFACs as automata models for quantum programs combining classical control flow with quantum-state operations, then studies their expressiveness and emptiness problem. It establishes an expressiveness hierarchy, a strict-versus-nonstrict decidability dichotomy, and a witness-searching procedure for one-loop QFACs.
- 1 Introduction: QFACs combine classical control flow with quantum operations, enabling automata-based analysis of quantum program configurations.Classical states track program control flow while quantum operations act throughout computation; emptiness asks whether a target configuration is reachable.
- 1 Introduction: Regular languages and QFA-definable languages are incomparable, while both are strictly less expressive than QFAC-definable languages.This result is stated under cut-point semantics for every non-trivial comparison operator and threshold.
- 1 Introduction: QFAC emptiness is decidable for strict thresholds and undecidable for non-strict thresholds.The result is obtained by reducing QFAC emptiness to emptiness of the intersection of a QFA and a finite automaton.
- 1 Introduction: Flat QFAC emptiness is related to the higher-dimensional orbit problem, while the status for flat and one-loop QFACs remains unclear.The paper specifically reduces one-loop QFAC emptiness, a subclass of flat QFACs, to that orbit problem.
- 1 Introduction: A template-free nonlinear-integer-programming procedure is sound and semi-complete for strict one-loop QFAC witness search.The procedure uses Taylor approximations of trigonometric functions and verifies generated witnesses with Mindtpy; experiments reach Grover search with 13 qubits and quantum random walks with 4 qubits.
2 Preliminaries
The preliminaries define QFAC structure, runs, acceptance probabilities, cut-point languages, and graph restrictions. They also illustrate how classical-state tracking and quantum rotations determine acceptance behavior.
- QFAC definition: A QFAC consists of a finite alphabet, classical states, an initial quantum state, symbol-indexed unitary matrices, state-indexed projections, and transitions.Deterministic and nondeterministic behavior is determined by the transition relation; a one-classical-state QFAC is a QFA.
- Flat QFACs: Flat QFACs have only simple-loop or single-vertex strongly connected components, and chains additionally restrict each component to at most one predecessor and successor.These graph restrictions exclude nested loops from the underlying automaton structure.
- Configurations and acceptance: A run follows transitions for an input word, while its acceptance probability is the squared norm after applying the word’s quantum operations and final-state projection.The word’s acceptance probability is the maximum over runs from the initial configuration.
- Example Aodd: In QFAC Aodd, each a rotates the state by one radian while b acts as identity, and the final state depends on the parity and count of a symbols.With projections selecting q1 and the x-axis, the acceptance probability is cos^2(n) for odd counts and 0 otherwise.
- Cut-point semantics: Cut-point languages classify words by comparing their acceptance probability with a threshold using strict or non-strict operators.The paper denotes languages such as L>λ(A), L<λ(A), L≥λ(A), and L≤λ(A), with trivial threshold/operator pairs excluded from substantive results.
3 Expressiveness
Under cut-point semantics, regular languages are strictly contained in QFAC-definable languages, while QFAs and regular languages are incomparable. The results also show that QFAC expressiveness depends on threshold type and underlying automaton structure.
- For every non-trivial threshold pair, some QFA-definable language is non-regular.
- For every non-trivial threshold pair, regular languages are a proper subclass of QFAC-definable languages.
- QFAs and regular languages are incomparable because a regular language excluding consecutive b's is not recognizable by any QFA.
- QFAC pumping differs from NFA pumping because the entire word is pumped rather than only an internal factor.
- Strict- and non-strict-threshold QFAC language classes are incomparable.
- QFACs with bideterministic underlying automata can be effectively simulated by QFAs without changing their threshold languages.
4 Decidability and Complexity of Emptiness
The paper characterizes QFAC emptiness: strict comparisons are decidable through reductions to QFA–finite-automaton intersections, while non-strict comparisons are undecidable. Structural restrictions yield decidable cases, orbit-problem connections, and complexity lower bounds.
- 4.1 Decidability for QFACs: For >, each QFAC state q yields a QFA A_q and NFA B_q whose language intersection equals the words reaching q above threshold.This decomposition enables the strict-case decidability result using known decidability for QFA intersections with linear context-free languages.
- 4.1 Decidability for QFACs: For <, subset construction tracks all reachable classical states, reducing emptiness to finitely many QFA intersections sharing initial states and unitary operators.The reduction checks each non-empty subset S of classical states and combines the resulting intersections to decide emptiness.
- 4.1 Decidability for QFACs: QFAC emptiness is decidable for strict comparisons > and <, but undecidable for non-strict comparisons ≥ and ≤.The strict cases reduce to intersections involving QFAs and finite automata; non-strict undecidability follows because QFAs are special cases of QFACs.
- 4.2 Decidability for Flat QFACs: Flat QFACs can be decomposed into chain QFACs; for chains, finite-order loop unitaries make equality-threshold emptiness decidable.Non-strict ≥ and ≤ cases reduce to strict emptiness together with equality-threshold emptiness.
- 4.2 Decidability for Flat QFACs: When λ = 1, one-loop QFAC emptiness is linked to the higher-dimensional orbit problem, while rank 0, 1, 2, n −2, n −1, or n projections give decidable cases.For 0 < λ < 1 and rank-one projections, the satisfying set is a union of two affine spaces; unary QFA emptiness inherits the listed rank-based decidability.
- 4.3 Complexity Lower Bounds: The emptiness problem is PSpace-hard for dimension 2, and remains NP-hard for flat QFACs and unary QFAs.One-loop QFACs decompose into |Q| unary QFAs, and the stated complexity lower bound extends to one-loop, flat, and finite-group QFACs.
5 An NIP-Based Algorithm for One-Loop QFAC
The paper reduces one-loop QFAC emptiness to nonlinear integer programming and relaxes trigonometric constraints with Taylor-based polynomial bounds. The resulting witness procedure is sound and uniformly semi-complete for strict thresholds, with experiments on rotation, Grover, and quantum-walk models.
- Implementation: The implementation searches incrementally over bounded-degree NIP instances and verifies candidate witnesses with MindtPy.The reported implementation uses Python 3.10 and a bounded approximation degree.
- Reduction to NIP: One-loop QFAC emptiness is reduced to an NIP problem whose objective contains a linear combination of cosine functions.Eigen-decomposition expresses the acceptance probability using computable real constants and trigonometric functions.
- Taylor relaxation: Taylor-series lower and upper polynomials replace cosine terms while preserving the relevant inequality ordering.The lower bound is used for > and ≥, while the upper bound is used for < and ≤.
- Soundness and completeness: The polynomial witnesses are sound and semi-complete for strict inequalities, with approximation degree increasing as needed.Increasing the Taylor order tightens the approximation; auxiliary periodicity variables make the semi-completeness uniform.
- Experiments: The experiments evaluate Simple-Rotation, Grover, and Quantum-Walk models with looped quantum operations and final measurements.Grover and Quantum-Walk vary the number of qubits and the reachable state being tested.
- Experiments: Most instances were solved within the time limit, while Grover scaled to many qubits and Quantum-Walk failed at five qubits.Large Grover instances spent most time in eigen-decomposition preprocessing; repeated eigenvalues may explain Grover’s easier optimization structure.
6 Conclusion
The conclusion establishes QFAC expressiveness and an emptiness decidability dichotomy under cut-point semantics. It also presents a sound, uniformly semi-complete NIP witness procedure for one-loop QFACs.
- Conclusion: QFAs and finite automata are incomparable in expressiveness, and both are strictly less expressive than QFACs.The conclusion also reports a QFAC pumping lemma distinguishing strict- and non-strict-threshold language classes.
- Conclusion: QFAC emptiness is decidable for strict thresholds and undecidable for non-strict thresholds.The result follows the corresponding decidability dichotomy known for QFAs.
- Complete QFACs: For non-strict comparisons, the construction assigns identity behavior to words with no valid runs and preserves the original acceptance probability otherwise.A naive sink construction cannot handle both cases correctly.
- Complete QFACs: The completeness construction combines sink-state and subset constructions to distinguish words with no valid runs from words with extendable runs.The resulting complete QFAC preserves the original language under the specified threshold and comparison operator.
B Missing Proofs of Section 3
These proofs establish QFAC expressiveness results, complement transformations, pumping behavior, and simulations by QFAs in restricted cases. They support the paper’s language-class comparisons and threshold arguments.
- Threshold transformations: Complementing projection operators transforms a deterministic QFAC language across the threshold and comparison operator.The construction replaces Pq with I − Pq and maps λ to 1 − λ.
- Expressiveness: For every non-trivial threshold pair, some QFA recognizes a non-regular language, so QFA languages strictly extend regular languages.The construction uses a two-dimensional QFA for unequal symbol counts and generalizes thresholds with an added dimension.
- Expressiveness: The language L¬(bb) and its complement are not recognizable by QFAs under strict cut-point semantics.The proof uses repeated insertions of bb to derive a contradiction with the assumed threshold separation.
- Pumping behavior: A QFAC has a pumping-style decomposition for sufficiently long accepted words, with a nonempty repeatable segment.The construction obtains repeated subset-construction states by the pigeonhole principle.
- QFA simulation: Bideterministic QFACs can be simulated by QFAs by encoding classical transitions as permutation matrices and retaining the quantum state in additional dimensions.The constructed QFA preserves acceptance probabilities for every word.
C.1 Missing Proofs of Section 4.1
The proofs reduce QFAC emptiness to finitely many QFA–automaton intersection problems and invoke decidability of strict-cutpoint intersections with linear context-free languages. This yields the strict/non-strict dichotomy.
- Reduction: For each QFAC state q, the language of words ending at q factors into a strict-cutpoint QFA language intersected with an NFA language.The QFA retains the quantum operators and projection Pq, while the NFA tracks paths ending at q.
- Strict thresholds: Strict-threshold emptiness for a QFAC is decidable by checking these intersections for every classical state.The number of states is finite, so the statewise checks combine into a decision procedure.
- Intersection decidability: Each NFA language can be represented as a linear context-free language, enabling use of the QFA–linear-context-free intersection result.The grammar construction has one nonterminal on each production’s right-hand side.
- Non-acceptance thresholds: For the < case, subset construction partitions words by their reachable classical-state set and requires every corresponding QFA acceptance value to remain below the threshold.Enumerating the finitely many reachable subsets yields decidability.
- Main result: The general QFAC emptiness problem is decidable for strict comparisons and undecidable for non-strict comparisons.Undecidability transfers immediately because QFAs are special cases of QFACs.
C.2 Missing Proofs of Section 4.2
A flat QFAC can be decomposed into finitely many chain QFACs while preserving its accepted language under each comparison relation and threshold.
- C.2 Missing Proofs of Section 4.2: A flat QFAC decomposes into chain QFACs A1, . . . , Am with the same accepted language.The decomposition is expressed as L▷◁λ(A) = ⋃ᵢ L▷◁λ(Aᵢ).
- C.2 Missing Proofs of Section 4.2: The proof organizes the underlying graph by strongly connected components and their ancestor–child relationships.Distinct child components can be removed while preserving the language, enabling repeated decomposition.
- C.2 Missing Proofs of Section 4.2: Repeatedly removing distinct child components yields a finite union of chain QFAC languages for every comparison relation and threshold.The construction applies uniformly for ▷◁ ∈ Cmp and λ ∈ [0, 1].
C.3 Missing Proofs of Section 4.3
This section establishes hardness results for QFAC decision problems by encoding finite-automaton behavior and Hamiltonian paths into two-dimensional quantum automata.
- C.3 Missing Proofs of Section 4.3: PSpace-hardness holds for QFAC universality even when the quantum dimension is 2.The construction combines several DFAs into a two-dimensional QFAC with identity quantum operations and accepting-state projections.
- C.3 Missing Proofs of Section 4.3: The union of DFAs is universal exactly when every word has an accepting QFAC run with probability at least λ.The reduction uses nondeterministic transitions from the initial state into the component DFAs.
- C.3 Missing Proofs of Section 4.3: NP-hardness holds for flat-QFAC emptiness through a reduction from the Hamiltonian path problem.For a directed graph G, a two-dimensional QFAC is constructed so that a word exceeds λ exactly when G has the required Hamiltonian path.
D Missing Proofs for Sections 5.1 and 5.2
The proofs characterize repeated quantum evolution using eigen-decomposition and polynomial bounds, enabling effective approximation arguments for threshold comparisons.
- D Missing Proofs for Sections 5.1 and 5.2: Eigen-decomposition expresses the acceptance probability using computable constants derived from the projection, unitary, and initial state.The eigenvalue phases and coefficient phases determine the oscillatory terms, and the parameters can be computed in O(n^3) time.
- D Missing Proofs for Sections 5.1 and 5.2: Taylor polynomials L_m and U_m provide lower and upper bounds for cos x, with the remainder shrinking as the degree increases.The bounds are established inductively from standard inequalities and the Lagrange remainder theorem.
- D Missing Proofs for Sections 5.1 and 5.2: For every ε > 0, sufficiently large approximation degree makes the polynomial bounds close enough to preserve the relevant threshold inequalities.The proof controls each pairwise oscillatory term and combines the bounds using a common degree M.
- D Missing Proofs for Sections 5.1 and 5.2: For each time t, phase representatives can be uniquely shifted by integer multiples of 2π into the interval [−π, π].This normalization supports the approximation argument for all comparison relations, including the corresponding < case.
E Implementation and Experiments Details
The implementation searches for bounded witnesses in one-loop QFACs using nonlinear integer programming and evaluates the procedure on rotation, Grover, and quantum-walk models.
- E Implementation and Experiments Details: Algorithm 1 takes a one-loop QFAC, a comparison–threshold pair, and a maximum approximation degree, then outputs an integer t.The search iterates over approximation degrees and imposes phase-normalization constraints involving integer variables K_ij.
- E Implementation and Experiments Details: Simple-Rotation tests fixed angles π/4, π/6, and π/8 for reaching |1⟩ from |0⟩ with probability greater than 0.99.This model uses a two-dimensional rotation matrix with a fixed rotation degree.
- E Implementation and Experiments Details: Grover tests whether a randomly selected oracle has success probability greater than 0.99 for some iteration count t.The model represents Grover’s algorithm for k qubits.
- E Implementation and Experiments Details: Quantum-Walk uses k qubits plus an ancilla coin qubit and tests whether a randomly generated state |x⟩ is reached with probability greater than 0.25.The modified walk is restricted to one direction rather than allowing movement in both directions.