Two-way Parikh Automata
Pith reviewed 2026-05-24 17:45 UTC · model grok-4.3
The pith
Emptiness for nondeterministic two-way Parikh automata is undecidable, but PSPACE-complete when visits per position are bounded and the constraint is an existential Presburger formula.
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
The paper shows that emptiness of nondeterministic two-way Parikh automata is undecidable. It is PSPACE-complete when the number of visits to any input position is bounded and the semi-linear set is given as an existential Presburger formula. Tight complexity bounds are established for the inclusion, equivalence and universality problems; the complexity of the same problems is characterized exactly when the semi-linear constraint is expressed by an arbitrary Presburger formula.
What carries the argument
Two-way Parikh automaton: a finite-state machine that traverses its input tape in both directions while maintaining counters tested only at the end against membership in a semi-linear set.
If this is right
- Emptiness is undecidable for nondeterministic two-way Parikh automata with no visit restriction.
- Emptiness, inclusion, equivalence and universality are all PSPACE-complete under bounded visits and existential Presburger constraints.
- When the semi-linear set is given by an arbitrary Presburger formula, the complexity of emptiness, inclusion, equivalence and universality is fully characterized.
- The decidability results rely on the semi-linear set being presented either existentially or via full Presburger arithmetic.
Where Pith is reading between the lines
- Transducer constructions that rely on Parikh automata may have to stay within one-way or bounded-visit fragments to preserve decidability of emptiness.
- Similar two-way extensions of other counter models with end-of-run constraints are likely to exhibit the same jump from decidable to undecidable emptiness.
- Bounded-visit restrictions could be enforced in practice by limiting the number of head reversals or by using deterministic two-way machines.
- The distinction between existential and full Presburger constraints may correspond to different fragments of linear arithmetic that appear in verification tools.
Load-bearing premise
The PSPACE upper bound for emptiness requires both a bound on the number of visits to each input position and an existential-Presburger presentation of the semi-linear set.
What would settle it
An algorithm that decides emptiness for nondeterministic two-way Parikh automata without any visit bound would falsify the undecidability claim.
read the original abstract
Parikh automata extend automata with counters whose values can only be tested at the end of the computation, with respect to membership into a semi-linear set. Parikh automata have found several applications, for instance in transducer theory, as they enjoy decidable emptiness problem. In this paper, we study two-way Parikh automata. We show that emptiness becomes undecidable in the non-deterministic case. However, it is PSpace-C when the number of visits to any input position is bounded and the semi-linear set is given as an existential Presburger formula. We also give tight complexity bounds for the inclusion, equivalence and universality problems. Finally, we characterise precisely the complexity of those problems when the semi-linear constraint is given by an arbitrary Presburger formula.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper studies two-way Parikh automata, which augment finite automata with counters whose final values are tested for membership in a semi-linear set. It proves that emptiness is undecidable for nondeterministic two-way Parikh automata. Under the additional restrictions that every input position is visited only a bounded number of times and that the semi-linear set is specified by an existential Presburger formula, emptiness is PSPACE-complete. The paper supplies tight complexity bounds for the inclusion, equivalence, and universality problems, and gives a precise characterization of the complexity of these problems when the semi-linear constraint is instead supplied by an arbitrary Presburger formula.
Significance. If the stated results hold, the work supplies a detailed complexity map for decision problems on two-way Parikh automata, extending the known decidability of emptiness for the one-way case and clarifying the effect of two-way head movement. The explicit reductions and automata constructions used to obtain the classifications constitute a concrete strength of the manuscript. The distinction drawn between existential and arbitrary Presburger presentations of the semi-linear set, together with the bounded-visit restriction, yields nuanced and useful information for applications in transducer theory and related areas of automata theory.
Simulated Author's Rebuttal
We thank the referee for the positive assessment of the manuscript and the recommendation to accept.
Circularity Check
No significant circularity in derivation chain
full rationale
The paper establishes undecidability of emptiness for nondeterministic two-way Parikh automata via explicit reductions, and PSPACE-completeness under bounded visits plus existential Presburger constraints via automata constructions. These are standard theoretical CS techniques relying on independent reductions to known problems rather than self-definitional equivalences, fitted parameters presented as predictions, or load-bearing self-citations. No step reduces by construction to its own inputs; the claims remain externally falsifiable through the cited reductions and constructions.
Axiom & Free-Parameter Ledger
axioms (2)
- standard math Decidability and complexity properties of Presburger arithmetic
- domain assumption Standard constructions and complexity results for two-way finite automata
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.