Deciding whether a fixed input clock stays close to a pushdown stack

30 September 2026. Working research note; complete written reduction relative to the primary results identified below. Not proof-assistant checked or independently reviewed. No claim of literature novelty.

1. Question and exact contract

When does an input-controlled clock provide enough information to maintain a persistent stack representation with bounded work per input letter? Earlier notes supplied a compiler given a bound, and finite certificates whenever a bound exists. Here the bound is not supplied.

The source P has finite control Q, finite input alphabet Sigma, finite stack alphabet Gamma, a nonempty finite set of initial states, and initially empty stack. Each rule consumes exactly one input letter, tests the top symbol or emptiness, and pushes one specified symbol, pops one symbol, or keeps the stack. Finite unions of guards are shorthand for separate rules. A pop at empty is either disabled or an explicitly permitted no-op. No epsilon rules, bulk updates, or other storage tests are allowed. Nondeterminism is allowed. Acceptance is existential and may inspect control and top/empty, but does not restrict the runs quantified below.

The given clock C consists of a complete finite observer R, initial r0, transition tau(r,a), and output c(r,a) in {-1,0,1}. It reads input only, independently of source choices, state and stack. Its numerical height is H0=0 and H’=max(0,H+c). In particular the observer cannot branch on H=0. Write h for actual source stack height, initially zero. All finite legal source runs and every prefix count, including rejecting and stuck prefixes.

Define, over these runs and prefixes,

U = sup(H-h),       V = sup(h-H),       Bmin = sup |h-H|.

The empty run ensures U,V >= 0. Values lie in N union {infinity}.

Theorem. Given the finite descriptions of P and C, boundedness of Bmin is decidable. On a positive instance the least bound Bmin is computable. More strongly, U and V are separately computable in N union {infinity}.

The hypotheses are finite syntactic conditions, not a presumed invariant or unknown bound. This is a characterization and decision of synchronization for this specified presentation and clock. It is only a sufficient route to persistent realization, not a characterization of all such realizations or a language-level impossibility test. No useful complexity bound is claimed.

2. When the clock leads: a weighted context-free language

For a fixed legal run of n steps let d_i=h_i-h_(i-1) be its actual increment, so d_i=0 at a permitted empty pop. Reflection gives

H_n = max_{0<=k<=n} sum_{i=k+1}^n c_i.

Proof: the empty suffix supplies zero; appending c takes the previous maximum plus c and then the maximum with zero, precisely the recurrence. Consequently

H_n-h_n = max_k (sum_{i=k+1}^n c_i - sum_{i=1}^n d_i).        (1)

Fold the observer into the source control. Split bottom rules so each annotated rule has a fixed actual d. Nondeterministically select one cut between source steps, including before the first or after the last step. Charge weight -d before the cut and c-d after it. This needs a finite phase bit and a weight-zero epsilon phase change. Permit stopping at any source configuration, not only an accepting one.

The language of legal annotated rule sequences with this cut is effectively context-free. For example, a PDA checks the sequence with the source stack, observer and phase; final-state acceptance leaves the stack unrestricted. The standard conversion to a grammar is effective. By (1), the supremum of total weights in this language is exactly U.

Use constructive Parikh equivalence [1] to obtain a finite automaton with the same vectors of terminal counts. Total weight is a fixed integer linear function of that vector, so its entire set of values is preserved. This does not preserve the rule-sequence language, input order or graph behavior. Give automaton edges their terminal weights, expanding word-labelled edges if needed, and trim to states on an initial-to-final path. A positive-weight cycle exists exactly when the accepted weights are unbounded above. If none exists, deleting cycles cannot decrease path weight, and the maximum occurs on a simple accepting path. Finite weighted-graph algorithms therefore compute U exactly, including infinity.

3. When the source leads: optional decrements and final draining

The other direction cannot use a freely selected cut: h_n-H_n is the minimum over the corresponding cuts. Supremum over runs does not turn that minimum into a maximum.

Instead construct a pushdown vector addition system with one nonnegative counter y (a 1-PVASS). Start with empty source stack and y=0. Retain exactly P’s stack guards and actions and C’s finite observer. During simulation all input letters are guessed and erased. For c=+1 increase y; for c=0 keep y; for c=-1 nondeterministically either keep y or decrement it, the latter enabled only when positive. No counter zero test is introduced.

Minimal-counter lemma. For each fixed source run and input prefix, every counter value reached this way is at least H; value H itself is attainable, with equality at every earlier prefix along one choice sequence.

Proof by induction. Increment and keep preserve the order. For c=-1, both available results from y>=H are at least max(0,H-1). Starting from equality, take decrement when positive and keep at zero. These choices do not change the source run, whose guards never inspect y. This proves both claims.

From any simulation-ready configuration, allow an irreversible switch to a matching phase. Pop one source symbol and decrement y together, any number t of times. Then irreversibly switch to an output phase, which pops each remaining source symbol, emitting one letter z per pop and keeping y. Accept only in the final state with empty stack and counter zero. The two phase switches do not test the counter. Incorrect guesses of t simply cannot satisfy the final counter condition.

Starting the drain at source height h and counter y, acceptance forces t=y. It is possible precisely when y<=h, and then emits z^(h-y). Stack symbols are unrestricted during draining; their guards remain enforced during simulation. A protected bottom marker implements empty-stack guards and is removed only at final acceptance, without emitting z. Private finite modes can split compound stack/counter operations. All these are ordinary offline PVASS operations; none is an added step of the real-time source or compiler.

Let D(P,C) be the resulting unary language. It contains epsilon. The lemma and drain calculation imply

sup {|v| : v in D(P,C)} = V.                              (2)

Indeed each output length h-y is at most h-H. Conversely every nonnegative gap h-H is emitted by choosing the minimal counter trajectory and draining H symbols before output. Negative gaps are irrelevant since V>=0. D may contain additional smaller lengths; equality of the suprema, not equality of the sets of actual nonnegative gaps, is the preservation claim.

4. Why the decision terminates

There are two routes, with different imported dependencies.

4.1 A decision using positive and negative finite evidence

The regular-stack certificate theorem in [4] semidecides Bmin<infinity: enumerate finite families of DFA rows K(q,r,e), and run the exact finite initialization, coordinate and transition-closure checks. A passing family is sound; completeness guarantees one whenever the skew is bounded.

For U=infinity the weighted construction in Section 2 is a decision test. For V=infinity, apply the effective run-embedding framework for PVASS in [2, Sections 3.1.4, 4.1 and 5]. It supplies enumerable finite accepting runs, decidable admissible embeddings, a well-quasi-order, and concatenative amalgamation. Thus unbounded unary output has a finite witness: two accepting runs rho embedded into sigma, with strictly larger output length in sigma. Amalgamation iterates the added output, so such a witness is sound. Conversely, unbounded output supplies runs of strictly increasing length; the well-quasi-order supplies an embedded pair. The embedding is the imported PVASS embedding, not arbitrary subsequence inclusion of traces.

Dovetail the positive certificate enumeration with this negative witness enumeration after the U test. If U is infinite, reject immediately. Otherwise a finite Bmin eventually produces a positive certificate; an infinite Bmin has infinite V and eventually produces a negative witness by (2). Soundness precludes conflicting answers. This proves termination without importing decidability of PVASS reachability. On a positive answer, test B=0,1,… using [4]’s complete fixed-bound procedure; the first success is Bmin.

Repeatability here is provided by the imported amalgamation property; recurrence of an appropriate pair follows separately from the well-quasi- order and unbounded unary lengths. This is a statement about accepting runs of the auxiliary PVASS. It supplies no unrestricted PEG pumping lemma and no recurrence theorem for arbitrary scaffold interfaces.

4.2 Computing each one-sided maximum

For the stronger assertion about V separately, [2, Main Theorem A] transfers decidable emptiness to effective downward closures. The one-counter PVASS language class satisfies its hypotheses: the paper supplies effective amalgamation, and a product with a finite transducer implements rational transductions without adding a counter. Epsilon output and private phases are permitted. Emptiness is fixed-configuration reachability, decidable by Biziere and Czerwinski [3, Theorem 1 and the PVAS/GVAS equivalence]. Their counter semantics prohibit negative intermediate values and prescribe the final value; they are exactly the semantics needed here.

Compute a finite automaton for the subword downward closure D(P,C) down. For a nonempty unary language this closure is either all z* or {epsilon,z,…,z^M}. A finite-automaton infiniteness test distinguishes them; in the finite case its maximum accepted length is M. Equation (2) gives V=infinity or V=M respectively. Together with Section 2 this computes both one-sided quantities and proves the stronger theorem. The 2024 paper’s then-open reachability discussion is not a current obstruction: [3] supplies the subsequently proved one-dimensional result.

5. Consequences and separating examples

For a positive pair (P,C), insert the computed Bmin into the earlier bounded- skew construction [5]. The construction stores a buffer of at most 2Bmin+1 source symbols over a synchronized core, applies established visibly pushdown determinization to the online observer annotation, and compiles the resulting deterministic immutable stack to a scaffold of degree two and native distance two, allocating one physical node per input letter. Initialization uses the reviewed fixed virtual base/missing root convention, with no added input letter. Acceptance is preserved at every same-word prefix, including epsilon; the corresponding PEG recognizes L(P)^R.

The buffer formula is a construction bound. Bmin is optimal only for the specified source/clock height disagreement; no minimal scaffold degree, radius, state count or memory encoding follows. The guarantee preserves decoded deterministic-stack behavior and fixed-controller acceptance, not each nondeterministic source history or arbitrary-context raw graph behavior. The offline algorithms have no claimed bounded-local-access resource limit.

For the independent push/keep example, a common input-clock height H would require both H<=B and n-H<=B, hence n<=2B, impossible for all n. This is a presentation obstruction, not a restriction on every presentation of x*.

For any given observer-state budget m, there are finitely many complete tables tau,c up to naming their at most m states. Enumerate and decide each by this theorem. Existence of a synchronizing clock within budget m is therefore decidable; a successful clock and its least skew are computable. Without a supplied budget, this enumeration still only semidecides clock existence. No finite sufficient observer-state budget is proved here.

6. Scope, failures, and next question

The substantive addition is the marked-cut and optional-decrement/drain reductions, their exact one-sided preservation statements, and their composition with established decision methods and the persistent compiler. Parikh equivalence, regular pushdown reachability, PVASS amalgamation and one-dimensional PVASS reachability are credited imports. Novelty of this particular composition has not been established by the literature search.

Do not replace the min over cuts by a max in the source-ahead direction. Do not allow the final drain to accept with a nonzero counter: that would accept z^h by skipping matching, even when h=H. Do not use skipped decrements to decide clock-ahead divergence: they can invent a large counter above H. Do not infer relative-skew boundedness from global stack boundedness of the auxiliary system, whose simulation stack may be unbounded even at skew zero.

The accompanying script checks only the elementary reductions on finite action histories, including empty-pop behavior, both skew identities, minimal optional-counter values, and the final drain. It does not implement Parikh conversion, PVASS embeddings/amalgamation, reachability, downward closures, unknown-bound decision, or the scaffold compiler. No finite experiment establishes the unbounded theorem. Its exact finite scope and results are in the recorded output.

The next substantive question is clock synthesis without a state budget: can one decide whether any finite input observer achieves bounded skew? The fixed-clock question is now settled by these reductions and must not be restarted as an open problem. Before pursuing synthesis, separate inherent variation between runs on one word from the additional requirement that one finite observer track the height through all input histories.

Primary dependencies

1. Javier Esparza, Pierre Ganty, Stefan Kiefer and Michael Luttenberger, Parikh’s Theorem: A simple and direct automaton construction, Information Processing Letters 111 (2011), Theorem 1.1. The effective count-preserving construction is the imported claim, not language equivalence. https://archive.model.in.tum.de/um/bibdb/esparza/IPL11.pdf
2. Ashwani Anand, Sylvain Schmitz, Lia Schuetze and Georg Zetzsche, Verifying Unboundedness via Amalgamation, LICS 2024, DOI 10.1145/3661814.3662133. Inspected author full version: Main Theorem A, Section 3.1.4, Section 4.1, and the explicit PVASS applicability statement in Section 1.2; Section 5 supplies the storage constructions. These are imported results, not independently reconstructed proofs. https://people.mpi-sws.org/~lschuetze/papers/verifying-unboundedness-via-amalgamation.pdf Publication record: https://lics.siglog.org/lics24/toc.html
3. Clotilde Biziere and Wojciech Czerwinski, Reachability in One-Dimensional Pushdown Vector Addition Systems is Decidable, STOC 2025, DOI 10.1145/3717823.3718149. Inspected author version: Theorem 1, PVAS/GVAS equivalence in the introduction, and Section 2 reachability semantics. The internal proof is imported. https://arxiv.org/html/2411.02386v1
4. Regular stack certificates, especially the fixed-bound first-exit procedure and complete certificate theorem; its classical regular-post* dependency is Schwoon (2002), Theorem 3.5.
5. Bounded stack skew and Inferred stack clocks, for the buffer, observer annotation, VPA determinization and scaffold resource contract. Foundational contracts separates observations.

The 2015 PVAS boundedness literature was also checked: global stack/counter boundedness and prefix-closed GVAS counter boundedness are different from the unary accepted-output problem used here. No direct transfer of those results is claimed. General residual, persistence, pointer simulation and uniformization comparisons remain as in the preceding notes; this run adds a precise verification connection, not a new unrestricted replay theory.